Reductive Logic and Proof-search Proof Theory, Semantics, and Control

by Pym, David J.; Ritter, Eike

• ISBN13: 9780198526339
• ISBN10: 0198526334
• Format: Hardcover
• Copyright: 2004-06-17
• Publisher: Clarendon Press

Summary

This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.

Table of Contents

Figures	xvi
Tables	xvii
1 Deductive Logic, Reductive Logic, and Proof-search	1	(26)
1.1 Introduction	1	(6)
1.2 Logical prerequisites	7	(8)
1.2.1 Basics of classical logic	7	(4)
1.2.2 Basics of intuitionistic logic	11	(2)
1.2.3 Basics of proof systems	13	(2)
1.3 Algebraic prerequisites	15	(8)
1.3.1 Basics of categories	16	(7)
1.4 Outline of the monograph	23	(1)
1.5 Discussion	24	(2)
1.6 Errata and remarks	26	(1)
2 Lambda-calculi for Intuitionistic and Classical Proofs	27	(30)
2.1 Introduction	27	(1)
2.2 Intuitionistic natural deduction	27	(5)
2.2.1 Sequential natural deduction	30	(1)
2.2.2 Natural deduction for intuitionistic predicate logic	31	(1)
2.3 The simply-typed λ-calculus	32	(6)
2.3.1 Normalization and subject reduction	36	(1)
2.3.2 λ-calculi and intuitionistic predicate logic	37	(1)
2.4 Classical natural deduction	38	(3)
2.5 The λμ-, λμ+-, λμν-, and λμνepsilon-calculi	41	(15)
2.5.1 Proof-objects and realizers	41	(1)
2.5.2 The λμ-calculus	42	(1)
2.5.3 Implication and conjunction	42	(3)
2.5.4 Disjunctive types: The λμν-calculus	45	(1)
2.5.5 The η-rules, strong normalization, and confluence	46	(6)
2.5.6 Explicit substitutions: The λμνepsilon-calculus	52	(4)
2.6 Discussion	56	(1)
3 The Semantics of Intuitionistic and Classical Proofs	57	(40)
3.1 Introduction	57	(1)
3.2 The semantics of intuitionistic proofs	57	(6)
3.2.1 Heyting algebras	59	(1)
3.2.2 Bi-Cartesian closed categories	60	(3)
3.3 Kripke semantics and functor categories	63	(4)
3.3.1 Kripke semantics	63	(3)
3.3.2 Functor categories	66	(1)
3.4 Games	67	(7)
3.4.1 Games for intuitionistic proofs	68	(6)
3.5 Fibred categories	74	(4)
3.6 The semantics of classical proofs	78	(13)
3.6.1 Boolean algebras	79	(1)
3.6.2 Models of classical proofs	80	(5)
3.6.3 Soundness and completeness for λμν	85	(1)
3.6.4 Continuations: Concrete, computational models	86	(3)
3.6.5 Games: Another concrete model	89	(2)
3.7 Comparing the disjunctions; De Morgan Laws	91	(4)
3.8 Discussion	95	(2)
4 Proof Theory for Reductive Logic	97	(53)
4.1 Introduction	97	(12)
4.2 Reductive proof theory	109	(6)
4.2.1 Background	110	(2)
4.2.2 Our perspective	112	(3)
4.3 Representation of sequent derivations in λμνepsilon	115	(3)
4.4 Intuitionistic provability	118	(4)
4.5 Uniform proof and analytic resolution	122	(10)
4.5.1 Uniform proofs	122	(2)
4.5.2 Permutations	124	(4)
4.5.3 Application to (hereditary Harrop) analytic resolution	128	(4)
4.6 Classical resolution	132	(9)
4.7 Intuitionistic resolution	141	(6)
4.7.1 Mints' intuitionistic resolution	141	(2)
4.7.2 The intuitionistic force of classical resolution	143	(4)
4.8 On complexity	147	(1)
4.9 Discussion	147	(3)
5 Semantics for Reductive Logic	150	(29)
5.1 Introduction	150	(1)
5.2 Semantics for intuitionistic reductive logic	151	(19)
5.2.1 Intuitionistic reduction models	158	(11)
5.2.2 Games for intuitionistic reductions	169	(1)
5.3 Semantics for classical reductive logic	170	(7)
5.3.1 Classical reduction models	171	(6)
5.4 Discussion	177	(2)
6 Intuitionistic and Classical Proof-search and Their Semantics	179	(18)
6.1 Introduction	179	(2)
6.2 Towards a semantics of control: Backtracking	181	(4)
6.3 A games semantics for proof-search	185	(8)
6.4 A concluding example: The semantics of uniform proof	193	(2)
6.5 Discussion	195	(2)
References	197	(8)
Index	205