Proof Analysis: A Contribution to Hilbert’s Last Problem

Title
Copyright
Contents
Preface
Prologue: Hilbert's last problem
1 Introduction
1.1 The idea of a proof
1.2 Proof analysis: an introductory example
(a) Natural deduction.
(b) The theory of equality.
1.3 Outline
(a) The four parts.
(b) Summary of the individual chapters.
I Proof systems based on natural deduction
2 Rules of proof: natural deduction
2.1 Natural deduction with general elimination rules
(a) Introduction rules as determined by the BHK-conditions.
(b) Inversion principle: determination of elimination rules.
(c) Discharge principle: definition of derivations.
(d) Derivable and admissible rules.
(e) Classical propositional logic.
2.2 Normalization of derivations
(a) Convertibility.
(b) Normal derivations.
(c) The subformula structure.
(d) The normalization of derivations.
(e) Strong normalization.
2.3 From axioms to rules of proof
(a) Mathematical rules.
(b) The subterm property.
(c) Complexity of derivations.
2.4 The theory of equality
(a) The rules of equality.
(b) Purely syntactic proofs of independence.
2.5 Predicate logic with equality and its word problem
(a) Replacement rules.
(b) The word problem.
Notes to Chapter 2
3 Axiomatic systems
3.1 Organization of an axiomatization
(a) Background to axiomatization.
(b) Projective geometry.
(c) Lattice theory.
3.2 Relational theories and existential axioms
Notes to Chapter 3
4 Order and lattice theory
4.1 Order relations
(a) Partial order.
(b) Strict partial order.
4.2 Lattice theory
(a) The subterm property.
(b) The Whitman conditions.
4.3 The word problem for groupoids
(a) The axioms and rules for a groupoid.
(b) The subterm property.
(c) Proof search.
(d) Functions.
4.4 Rule systems with eigenvariables
(a) Lattice theory.
(b) Strict order with equality.
Notes to Chapter 4
5 Theories with existence axioms
5.1 Existence in natural deduction
5.2 Theories of equality and order again
(a) Non-triviality in equality.
(b) Non-degenerate partial order.
5.3 Relational lattice theory
(a) The rules of relational lattice theory.
(b) Permutability of rules.
(c) Derivability of universal formulas.
(d) Further decidable classes of formulas.
Notes to Chapter 5
II Proof systems based on sequent calculus
6 Rules of proof: sequent calculus
6.1 From natural deduction to sequent calculus
(a) Notation and rules for sequent calculus.
(b) `Sequents as sets'.
(c) Desiderata on sequent calculi.
(d) Classical propositional logic.
(e) Multisuccedent sequents.
(f) Sequent calculi with invertible rules.
(g) Rules for the quantifiers.
6.2 Extensions of sequent calculus
(a) Cut elimination in the presence of axioms.
(b) Four approaches to extension by axioms.
(c) Complexity of derivations.
6.3 Predicate logic with equality
6.4 Herbrand's theorem for universal theories
Notes to Chapter 6
7 Linear order
7.1 Partial order and Szpilrajn's theorem
(a) Minimal derivations.
(b) Partial order.
(c) Linear order.
(d) Extension algorithm from partial to linear order.
7.2 The word problem for linear order
(a) Systems of right rules.
(b) Linear order.
7.3 Linear lattices
Notes to Chapter 7
III Proof systems for geometric theories
8 Geometric theories
8.1 Systems of geometric rules
(a) The geometric rule scheme.
(b) Examples of geometric theories.
8.2 Proof theory of geometric theories
8.3 Barr's theorem
Notes to Chapter 8
9 Classical and intuitionistic axiomatics
9.1 The duality of classical and constructive notions and proofs
(a) Finitary basic concepts.
(b) Derivations in left and right rule systems.
9.2 From geometric to co-geometric axioms and rules
9.3 Duality of dependent types and degenerate cases
Notes to Chapter 9
10 Proof analysis in elementary geometry
10.1 Projective geometry
(a) Basic relations, constructions, and axioms.
(b) Multiple-conclusion rules.
(c) The rules of projective geometry.
(d) The subterm property.
10.2 Affine geometry
10.3 Examples of proof analysis in geometry
Notes to Chapter 10
IV Proof systems for non-classical logics
11 Modal logic
11.1 The language and axioms of modal logic
11.2 Kripke semantics
11.3 Formal Kripke semantics
(a) Basic modal logic.
(b) Extensions.
11.4 Structural properties of modal calculi
11.5 Decidability
11.6 Modal calculi with equality, undefinability results
11.7 Completeness
(a) Soundness.
(b) Completeness.
Notes to Chapter 11
12 Quantified modal logic, provability logic, & other non-classical log ics
12.1 Adding the quantifiers
(a) Semantics and syntax of quantified modal logic.
(b) Structural properties.
(c) Soundness and completeness.
12.2 Provability logic
12.3 Intermediate logics
12.4 Substructural logics
Notes to Chapter 12
Bibliography
Index of names
Index of subjects