Interpolation and Definability Modal and Intuitionistic Logic

by Gabbay, Dov M.; Maksimova, Larisa

• ISBN13: 9780198511748
• ISBN10: 0198511744
• Format: Hardcover
• Copyright: 2005-07-28
• Publisher: Clarendon Press

Summary

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.

Table of Contents

1 Introduction and discussion	1	(34)
1.1 General discussion	1	(13)
1.1.1 View 1: Common logical content	2	(1)
1.1.2 View 2: Expressive power	2	(2)
1.1.3 View 3: Quantifier elimination	4	(2)
1.1.4 View 4: Artificial intelligence	6	(1)
1.1.5 View 5: Proof theory	6	(1)
1.1.6 View 6: Consistency	7	(1)
1.1.7 View 7: Semantical view	8	(1)
1.1.8 View 8: Algebraic view	9	(3)
1.1.9 View 9: Definability	12	(1)
1.1.10 View 10: Interpolation by translation	13	(1)
1.1.11 View 11: Traditional studies	14	(1)
1.1.12 Concluding remarks	14	(1)
1.2 Interpolation in general logics	14	(11)
1.2.1 Historical background	14	(1)
1.2.2 General logics and interpolation	15	(10)
1.3 Overview of the book	25	(10)
2 Modal and superintuitionistic logics: basic concepts	35	(26)
2.1 Introduction overview	35	(1)
2.2 The Kripke semantics for quantified modal and intermediate logics	35	(15)
2.2.1 Propositional modal logics	36	(5)
2.2.2 Propositional intermediate logics	41	(2)
2.2.3 Quantified modal logics	43	(5)
2.2.4 Quantified superintuitionistic logics	48	(2)
2.3 Algebraic interpretation of propositional logics	50	(6)
2.3.1 Pseudoboolean algebras	50	(3)
2.3.2 Modal algebras	53	(3)
2.4 Inter-relation of relational and algebraic semantics	56	(5)
2.4.1 From the Kripke semantics to the algebraic one	57	(1)
2.4.2 Representation theorems	58	(3)
3 Superintuitionistic logics and normal extensions of the modal logics S4	61	(42)
3.1 Translation	61	(9)
3.1.1 Pseudoboolean and topoboolean algebras	61	(5)
3.1.2 Lattice of superintuitionistic logics and NE(S4)	66	(4)
3.2 A classification of normal extensions of S4 according to their superintuitionistic fragments	70	(9)
3.2.1 Characteristic formulas of pre-ordered frames	70	(3)
3.2.2 Some properties of the classification	73	(6)
3.3 Well-representable logics	79	(10)
3.3.1 Algebras and pre-ordered frames	79	(1)
3.3.2 Representing frames	80	(4)
3.3.3 Well-representable logics and varieties	84	(5)
3.4 Classification by slices	89	(5)
3.5 Finite pseudoboolean and topoboolean algebras	94	(9)
3.5.1 Finite algebras and finite frames	94	(3)
3.5.2 Characteristic formulas of Gödelian pseudoboolean and topoboolean algebras	97	(3)
3.5.3 Logics LC and KC	100	(3)
4 The interpolation theorem in intuitionistic predicate calculus	103	(26)
4.1 Interpolation in classical predicate logic	103	(7)
4.1.1 Craig's interpolation and Robinson's joint consistency	103	(3)
4.1.2 Lyndon's interpolation	106	(4)
4.2 Interpolation theorem in the intuitionistic logic	110	(11)
4.2.1 Definitions	110	(3)
4.2.2 Robinson's theorem	113	(6)
4.2.3 Equivalence of CIP and RCP	119	(2)
4.3 Propositional intermediate logics	121	(3)
4.4 Notes	124	(1)
4.5 Implicit and explicit definability	125	(4)
5 Interpolation and definability in quantified logics	129	(42)
5.1 Inter-relations between interpolation, definability, and joint consistency	129	(3)
5.2 Lyndon's interpolation in some modal systems	132	(8)
5.2.1 LIP in quantified logics	132	(7)
5.2.2 Lyndon's interpolation in propositional modal logics	139	(1)
5.3 The Craig interpolation in modal logics	140	(9)
5.3.1 Modal logics without LIP	140	(2)
5.3.2 Craig's interpolation in some modal logics	142	(7)
5.4 Failure of interpolation	149	(3)
5.5 Preserving interpolation and definability	152	(8)
5.5.1 Axioms preserving interpolation	153	(4)
5.5.2 Interpolation and intersection of logics	157	(3)
5.6 First-order logics with equality	160	(11)
5.6.1 Preliminaries	161	(1)
5.6.2 Formulas preserving interpolation	162	(3)
5.6.3 Modal logics	165	(1)
5.6.4 A counter-example	166	(2)
5.6.5 Functional symbols	168	(3)
6 Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudoboolean algebras	171	(34)
6.1 Craig's theorem and amalgamation property	172	(5)
6.2 Amalgamable varieties of PBA	177	(6)
6.3 Characterization of the varieties H1-H8	183	(2)
6.4 Necessary conditions for varieties of PBA to be amalgamable	185	(14)
6.5 Logics with Craig's interpolation property	199	(4)
6.6 Positive logics	203	(2)
7 Interpolation, definability, amalgamation	205	(20)
7.1 Inter-relation of Beth's and Craig's properties in propositional logics	205	(6)
7.2 Varieties of modal algebras	211	(14)
7.2.1 Interpolation, implicit and explicit definability	211	(2)
7.2.2 The Beth property, interpolation, amalgamation in varieties	213	(9)
7.2.3 Independence of amalgamation property and the Beth property in equational theories of modal algebras	222	(3)
8 Interpolation in normal extensions of the modal logic S4	225	(40)
8.1 Interpolation and amalgamability	226	(1)
8.2 Necessary conditions for amalgamability	227	(12)
8.3 Classification of varieties of topoboolean algebras	239	(2)
8.4 Interpolation theorems in modal logics	241	(2)
8.5 Sufficient conditions for amalgamation	243	(12)
8.5.1 Well-representable logics and varieties	244	(3)
8.5.2 Sufficient conditions for amalgamability and superamalgamability	247	(1)
8.5.3 Lemmas on (α1, α2)-products	248	(4)
8.5.4 Stable and superstable classes of frames	252	(3)
8.6 Logics with interpolation in NE(S4)	255	(2)
8.7 Decidability of interpolation over S4	257	(1)
8.8 NE(S4) versus E(Int)	258	(7)
8.8.1 More on Gödel's translation	259	(2)
8.8.2 IPN in NE(S4)	261	(4)
9 Complexity of some problems in modal and intuitionistic calculi	265	(20)
9.1 Main results	265	(2)
9.2 Reducibilities	267	(2)
9.3 Complexity	269	(3)
9.4 Tabularity and related properties	272	(5)
9.5 Interpolation and amalgamation	277	(8)
10 Interpolation in modal infinite slice logics containing the logic K4	285	(26)
10.1 K4 and S4	285	(2)
10.2 Logics and varieties of infinite slice	287	(6)
10.3 Necessary condition of interpolation	293	(18)
11 An analogue of Beth's theorem in normal extensions of the modal logic K4	311	(22)
11.1 Preliminaries	311	(2)
11.2 The Replacement theorem and its corollaries	313	(2)
11.3 The main theorem	315	(12)
11.3.1 Case 1	318	(3)
11.3.2 Case 2	321	(6)
11.4 A counter-example to the Beth property	327	(1)
11.5 Explicit definitions	328	(5)
11.5.1 Logics of finite slices	329	(2)
11.5.2 Constructing explicit definitions	331	(2)
12 Extensions of the provability logic	333	(38)
12.1 Two extensions of G	333	(5)
12.2 Interpolation in infinite-slice extensions of provability logic	338	(15)
12.2.1 Definitions and notations	338	(2)
12.2.2 Description of Gγ and Gδ	340	(7)
12.2.3 Interpolation theorem	347	(6)
12.3 Continuum of extensions of the provability logic with interpolation	353	(10)
12.3.1 Interpolation and amalgamation properties	354	(1)
12.3.2 The Logic Gλ	355	(3)
12.3.3 Continuum of extensions of the logic Gλ that have the Craig interpolation property	358	(3)
12.3.4 Amalgamation and superamalgamation properties	361	(2)
12.4 Boxed formulas	363	(8)
12.4.1 Preliminaries	363	(1)
12.4.2 The main lemmas	364	(2)
12.4.3 CIP and IPB	366	(3)
12.4.4 The property B2	369	(2)
13 Syntactic proof of interpolation for the intuitionistic predicate logic	371	(10)
13.1 Formal system S	371	(2)
13.2 Proof of interpolation	373	(6)
13.3 Fragments of IntQ	379	(2)
14 Interpolation by translation	381	(22)
14.1 Introduction	381	(3)
14.2 Interpolation by quantifier elimination	384	(4)
14.2.1 SCAN: Second-order quantifier elimination	384	(1)
14.2.2 SCAN can interpolate	385	(3)
14.3 Case study: Quantified S5	388	(9)
14.3.1 Preliminary discussion	388	(2)
14.3.2 Interpolation for QS5	390	(7)
14.4 Case study: Propositional modal logic S4.3	397	(1)
14.5 Interpolation by translation: General theory	398	(5)
15 Interpolation in (intuitionistic) logic programming	403	(22)
15.1 Introduction	403	(1)
15.2 N-prolog	404	(5)
15.3 Interpolation for propositional Horn programs	409	(3)
15.4 Alternative proof	412	(2)
15.5 Controlled interpolation for propositional Horn clauses	414	(2)
15.6 Failure of interpolation for fragment of predicate intuitionistic logic	416	(2)
15.7 Weak interpolation for intuitionistic logic programs	418	(7)
16 Interpolation in goal-directed proof systems	425	(46)
16.1 Introduction	425	(7)
16.1.1 General background	425	(2)
16.1.2 Specific background	427	(5)
16.2 Interpolation for linear and for intuitionistic implication	432	(6)
16.2.1 Interpolation for linear implication	432	(3)
16.2.2 Interpolation for intuitionistic logic	435	(3)
16.2.3 Interpolation for classical logic	438	(1)
16.3 Interpolation for the Lambek calculus	438	(7)
16.4 Interpolation for strict implication	445	(19)
16.5 Concluding discussion, chain interpolation	464	(7)
16.5.1 Structural interpolation	464	(2)
16.5.2 Chain interpolation	466	(2)
16.5.3 Beth definability	468	(1)
16.5.4 Standard interpolation in classical logic	469	(1)
16.5.5 Concluding remarks	470	(1)
17 Further results and discussion	471	(12)
17.1 Introduction	471	(1)
17.2 Further results	471	(7)
17.2.1 Temporal logics	472	(1)
17.2.2 Beth properties and epimorphisms surjectivity	472	(1)
17.2.3 Projective Beth property over Int	473	(1)
17.2.4 Positive and paraconsistent logics	473	(1)
17.2.5 Modal logics and projective Beth property	474	(1)
17.2.6 Restricted interpolation and restricted amalgamation	475	(1)
17.2.7 Variable separation	476	(1)
17.2.8 Decidable properties of logics and of varieties	477	(1)
17.3 Further discussion	478	(5)
17.3.1 Interpolation and artificial intelligence	478	(1)
17.3.2 Interpolation for classical theories	478	(1)
17.3.3 A semantic/categorial engine for interpolation	478	(1)
17.3.4 Interpolation in computer science	479	(1)
17.3.5 Case study: Implementation of constant domains modal K4 in classical logic	480	(3)
Appendix	483	(1)
References	484	(19)
Index	503