Quantification and modalities have always been topics of great interest for logicians. These two themes emerged from philosophy andlanguage in ancient times; they were studied by traditional informalmethods until the 20th century. In the last century the tools becamehighly mathematical, and both modal logic and quantification found numerous applications in Computer Science. At the same time many other kinds of nonclassical logics were investigated and applied to Computer Science. Although there exist several good books in propositional modal logics, this book is the first detailed monograph in nonclassical first-order quantification. It includes results obtained during the past thirty years. The field is very large, so we confine ourselves with only two kinds of logics: modal and superintuitionistic. The main emphasis of Volume 1 is model-theoretic, and it concentrates on descriptions of different sound semantics and completeness problem --- even for these seemingly simple questions we have our hands full. The major part of the presented material has never been published before. Some results are very recent, and for other results we either give new proofs or first proofs in full detail.
Author(s): Dov M. Gabbay, Dimitrij Skvortsov, Valentin Shehtman
Series: Studies in Logic and the Foundations of Mathematics, Volume 153
Publisher: Elsevier
Year: 2009
Language: English
Pages: 640
Title ......Page 3
Copyright ......Page 4
Preface ......Page 5
Introduction ......Page 9
Contents ......Page 21
Part I Preliminaries ......Page 25
1.1.1 Formulas ......Page 27
1.1.2 Logics ......Page 29
1.2 Algebraic semantics ......Page 35
1.3.2 Kripke frames and models ......Page 43
1.3.3 Main constructions ......Page 48
1.3.4 Conical expressiveness ......Page 54
1.4 Relational semantics (the intuitionistic case) ......Page 56
1.5 Modal counterparts ......Page 61
1.6 General Kripke frames ......Page 62
1.7 Canonical Kripke models ......Page 64
1.8 First-order translations and definability ......Page 68
1.9 Some general completeness theorems ......Page 71
1.10 Trees and unravelling ......Page 72
1.11 PTC-logics and Horn closures ......Page 76
1.12 Subframe and cofinal subframe logics ......Page 82
1.13 Splittings ......Page 89
1.14 Tabularity ......Page 92
1.15 Transitive logics of finite depth ......Page 94
1.16 delta-operation ......Page 96
1.17 Neighbourhood semantics ......Page 100
2.1 Introduction ......Page 103
2.2 Formulas ......Page 105
2.3 Variable substitutions ......Page 109
2.4 Formulas with constants ......Page 126
2.5 Formula substitutions ......Page 129
2.6 First-order logics ......Page 143
2.7 First-order theories ......Page 163
2.8 Deduction theorems ......Page 166
2.9 Perfection ......Page 170
2.10 Intersections ......Page 175
2.11 Goedel-Tarski translation ......Page 177
2.12 The Glivenko theorem ......Page 181
2.13 Aoperation ......Page 182
2.14 Adding equality ......Page 196
2.15 Propositional parts ......Page 204
2.16 Semantics from an abstract viewpoint ......Page 209
Part II Semantics ......Page 215
Introduction: What is semantics? ......Page 217
3.1 Preliminary discussion ......Page 223
3.2 Predicate Kripke frames ......Page 229
3.3 Morphisms of Kripke frames ......Page 243
3.4 Constant domains ......Page 254
3.5.1 Introduction ......Page 258
3.5.2 Kripke frames with equality ......Page 259
3.5.3 Strong morphisms ......Page 263
3.5.4 Main constructions ......Page 265
3.6 Kripke sheaves ......Page 267
3.7 Morphisms of Kripke sheaves ......Page 277
3.8 Transfer of completeness ......Page 283
3.9 Simulation of varying domains ......Page 290
3.10 Examples of Kripke semantics ......Page 292
3.11.1 Modal case ......Page 301
3.11.2 Intuitionistic case ......Page 303
3.12 Translations into classical logic ......Page 305
4.1 Modal and Heyting valued structures ......Page 317
4.2 Algebraic models ......Page 325
4.3 Soundness ......Page 335
4.4 Morphisms of algebraic structures ......Page 343
4.5 Presheaves and omega-sets ......Page 352
4.6 Morphisms of presheaves ......Page 357
4.7 Sheaves ......Page 362
4.8 Fibrewise models ......Page 363
4.9 Examples of algebraic semantics ......Page 365
5.1 Preliminary discussion ......Page 369
5.2 Kripke bundles ......Page 375
5.3 More on forcing in Kripke bundles ......Page 380
5.4 Morphisms of Kripke bundles ......Page 383
5.5 Intuitionistic Kripke bundles ......Page 389
5.6 Functor semantics ......Page 398
5.7 Morphisms of presets ......Page 405
5.8 Bundles over precategories ......Page 410
5.9 Metaframes ......Page 412
5.10 Permutability and weak functoriality ......Page 421
5.11 Modal metaframes ......Page 428
5.12 Modal soundness ......Page 433
5.13 Representation theorem for modal metaframes ......Page 443
5.14.1 Intuiutionistic forcing ......Page 446
5.14.2 Monotonic metaframes ......Page 453
5.15 Intuitionistic soundness ......Page 456
5.16 Maximality theorem ......Page 476
5.17 Kripke quasi-bundles ......Page 489
5.18 Some constructions on metaframes ......Page 491
5.19 On semantics of intuitionistic sound metaframes ......Page 493
5.20 Simplicial frames ......Page 497
Part III Completeness ......Page 505
6.1 Canonical models for modal logics ......Page 507
6.2 Canonical models for superintuitionistic logics ......Page 517
6.3 Intermediate logics of finite depth ......Page 525
6.4 Natural models ......Page 528
6.5 Refined completeness theorem for QH + KF ......Page 539
6.6 Directed frames ......Page 540
6.7 Logics of linear frames ......Page 548
6.8 Properties of delta-operation ......Page 552
6.9 delta-operation preserves completeness ......Page 556
6.10 Trees of bounded branching and depth ......Page 560
6.11 Logics of uniform trees ......Page 563
7.1 Modal canonical models with constant domains ......Page 577
7.2 Intuitionistic canonical models with constant domains ......Page 579
7.3 Some examples of C-canonical logics ......Page 582
7.4 Predicate versions of subframe and tabular logics ......Page 587
7.5 Predicate versions of cofinal subframe logics ......Page 589
7.6 Natural models with constant domains ......Page 597
7.7 Remarks on Kripke bundles with constant domains ......Page 601
7.8 Kripke frames over the reals and the rationals ......Page 603
Bibliography ......Page 617
Index ......Page 627
Cover ......Page 640
