This monograph is on interpolation and definability, a notion central in pure logic and with significant meaning and applicability in all areas where logic is applied, especially computer science, artificial intelligence, logic programming, philosophy of science and natural language. Suitable for researchers and graduate students in mathematics, computer science and philosophy, this is the latest in the prestigious world-renowned Oxford Logic Guides, which contains Michael Dummet's Elements of Intuitionism (Second Edition), J.M. Dunn and G. Hardegree's Algebraic Methods in Philosophical Logic, H. Rott's Change Choice and Inference: A Study of Belief Revision and Nonmonotonic Reasoning, P.T. Johnstone's Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2, and David J. Pym and Eike Ritter's Reductive Logic and Proof Search: Proof, Theory, Semantics and Control.
Author(s): Dov M. Gabbay, Larisa Maksimova
Series: Oxford Logic Guides 46
Publisher: Oxford University Press
Year: 2005
Language: English
Pages: 524
Contents......Page 11
1.1 General discussion......Page 17
1.1.2 View 2: Expressive power......Page 18
1.1.3 View 3: Quantifier elimination......Page 20
1.1.5 View 5: Proof theory......Page 22
1.1.6 View 6: Consistency......Page 23
1.1.7 View 7: Semantical view......Page 24
1.1.8 View 8: Algebraic view......Page 25
1.1.9 View 9: Definability......Page 28
1.1.10 View 10: Interpolation by translation......Page 29
1.2.1 Historical background......Page 30
1.2.2 General logics and interpolation......Page 31
1.3 Overview of the book......Page 41
2.2 The Kripke semantics for quantified modal and intermediate logics......Page 51
2.2.1 Propositional modal logics......Page 52
2.2.2 Propositional intermediate logics......Page 57
2.2.3 Quantified modal logics......Page 59
2.2.4 Quantified superintuitionistic logics......Page 64
2.3.1 Pseudoboolean algebras......Page 66
2.3.2 Modal algebras......Page 69
2.4 Inter-relation of relational and algebraic semantics......Page 72
2.4.1 From the Kripke semantics to the algebraic one......Page 73
2.4.2 Representation theorems......Page 74
3.1.1 Pseudoboolean and topoboolean algebras......Page 77
3.1.2 Lattice of superintuitionistic logics and NE(S4)......Page 82
3.2.1 Characteristic formulas of pre-ordered frames......Page 86
3.2.2 Some properties of the classification......Page 89
3.3.1 Algebras and pre-ordered frames......Page 95
3.3.2 Representing frames......Page 96
3.3.3 Well-representable logics and varieties......Page 100
3.4 Classification by slices......Page 105
3.5.1 Finite algebras and finite frames......Page 110
3.5.2 Characteristic formulas of Gödelian pseudoboolean and topoboolean algebras......Page 113
3.5.3 Logics LC and KC......Page 116
4.1.1 Craig's interpolation and Robinson's joint consistency......Page 119
4.1.2 Lyndon's interpolation......Page 122
4.2.1 Definitions......Page 126
4.2.2 Robinson's theorem......Page 129
4.2.3 Equivalence of CIP and RCP......Page 135
4.3 Propositional intermediate logics......Page 137
4.4 Notes......Page 140
4.5 Implicit and explicit definability......Page 141
5.1 Inter-relations between interpolation, definability, and joint consistency......Page 145
5.2.1 LIP in quantified logics......Page 148
5.2.2 Lyndon's interpolation in propositional modal logics......Page 155
5.3.1 Modal logics without LIP......Page 156
5.3.2 Craig's interpolation in some modal logics......Page 158
5.4 Failure of interpolation......Page 165
5.5 Preserving interpolation and definability......Page 168
5.5.1 Axioms preserving interpolation......Page 169
5.5.2 Interpolation and intersection of logics......Page 173
5.6 First-order logics with equality......Page 176
5.6.1 Preliminaries......Page 177
5.6.2 Formulas preserving interpolation......Page 178
5.6.3 Modal logics......Page 181
5.6.4 A counter-example......Page 182
5.6.5 Functional symbols......Page 184
6 Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudoboolean algebras......Page 187
6.1 Craig's theorem and amalgamation property......Page 188
6.2 Amalgamable varieties of PBA......Page 193
6.3 Characterization of the varieties H[sub(1)]–H[sub(8)]......Page 199
6.4 Necessary conditions for varieties of PBA to be amalgamable......Page 201
6.5 Logics with Craig's interpolation property......Page 215
6.6 Positive logics......Page 219
7.1 Inter-relation of Beth's and Craig's properties in propositional logics......Page 221
7.2.1 Interpolation, implicit and explicit definability......Page 227
7.2.2 The Beth property, interpolation, amalgamation in varieties......Page 229
7.2.3 Independence of amalgamation property and the Beth property in equational theories of modal algebras......Page 238
8 Interpolation in normal extensions of the modal logic S4......Page 241
8.1 Interpolation and amalgamability......Page 242
8.2 Necessary conditions for amalgamability......Page 243
8.3 Classification of varieties of topoboolean algebras......Page 255
8.4 Interpolation theorems in modal logics......Page 257
8.5 Sufficient conditions for amalgamation......Page 259
8.5.1 Well-representable logics and varieties......Page 260
8.5.2 Sufficient conditions for amalgamability and superamalgamability......Page 263
8.5.3 Lemmas on (a-[sub(1)], a[sub(2)])-products......Page 264
8.5.4 Stable and superstable classes of frames......Page 268
8.6 Logics with interpolation in NE(S4)......Page 271
8.7 Decidability of interpolation over S4......Page 273
8.8 NE(S4) versus E(Int)......Page 274
8.8.1 More on Gödel's translation......Page 275
8.8.2 IPN in NE(S4)......Page 277
9.1 Main results......Page 281
9.2 Reducibilities......Page 283
9.3 Complexity......Page 285
9.4 Tabularity and related properties......Page 288
9.5 Interpolation and amalgamation......Page 293
10.1 K4 and S4......Page 301
10.2 Logics and varieties of infinite slice......Page 303
10.3 Necessary condition of interpolation......Page 309
11.1 Preliminaries......Page 327
11.2 The Replacement theorem and its corollaries......Page 329
11.3 The main theorem......Page 331
11.3.1 Case 1......Page 334
11.3.2 Case 2......Page 337
11.4 A counter-example to the Beth property......Page 343
11.5 Explicit definitions......Page 344
11.5.1 Logics of finite slices......Page 345
11.5.2 Constructing explicit definitions......Page 347
12.1 Two extensions of G......Page 349
12.2.1 Definitions and notations......Page 354
12.2.2 Description of Gγ and Gδ......Page 356
12.2.3 Interpolation theorem......Page 364
12.3 Continuum of extensions of the provability logic with interpolation......Page 369
12.3.1 Interpolation and amalgamation properties......Page 370
12.3.2 The Logic Gγ......Page 371
12.3.3 Continuum of extensions of the logic Gγ that have the Craig interpolation property......Page 374
12.3.4 Amalgamation and superamalgamation properties......Page 377
12.4.1 Preliminaries......Page 379
12.4.2 The main lemmas......Page 380
12.4.3 CIP and IPB......Page 382
12.4.4 The property B2......Page 385
13.1 Formal system S......Page 387
13.2 Proof of interpolation......Page 389
13.3 Fragments of IntQ......Page 395
14.1 Introduction......Page 397
14.2.1 SCAN: Second-order quantifier elimination......Page 400
14.2.2 SCAN can interpolate......Page 401
14.3.1 Preliminary discussion......Page 404
14.3.2 Interpolation for QS5......Page 406
14.4 Case study: Propositional modal logic S4.3......Page 413
14.5 Interpolation by translation: General theory......Page 414
15.1 Introduction......Page 419
15.2 N-prolog......Page 420
15.3 Interpolation for propositional Horn programs......Page 425
15.4 Alternative proof......Page 428
15.5 Controlled interpolation for propositional Horn clauses......Page 430
15.6 Failure of interpolation for ∀-⊃ fragment of predicate intuitionistic logic......Page 432
15.7 Weak interpolation for intuitionistic logic programs......Page 434
16.1.1 General background......Page 441
16.1.2 Specific background......Page 443
16.2.1 Interpolation for linear implication......Page 448
16.2.2 Interpolation for intuitionistic logic......Page 451
16.3 Interpolation for the Lambek calculus......Page 454
16.4 Interpolation for strict implication......Page 461
16.5.1 Structural interpolation......Page 480
16.5.2 Chain interpolation......Page 482
16.5.3 Beth definability......Page 484
16.5.4 Standard interpolation in classical logic......Page 485
16.5.5 Concluding remarks......Page 486
17.2 Further results......Page 487
17.2.2 Beth properties and epimorphisms surjectivity......Page 488
17.2.4 Positive and paraconsistent logics......Page 489
17.2.5 Modal logics and projective Beth property......Page 490
17.2.6 Restricted interpolation and restricted amalgamation......Page 491
17.2.7 Variable separation......Page 492
17.2.8 Decidable properties of logics and of varieties......Page 493
17.3.3 A semantic/categorial engine for interpolation......Page 494
17.3.4 Interpolation in computer science......Page 495
17.3.5 Case study: Implementation of constant domains modal K4 in classical logic......Page 496
Appendix......Page 499
References......Page 500
Index......Page 519
D......Page 520
H......Page 521
L......Page 522
R......Page 523
Z......Page 524
