Proof Analysis: A Contribution to Hilbert’s Last Problem

Cover......Page 1
Title......Page 5
Copyright......Page 6
Contents......Page 7
Preface......Page 11
Prologue: Hilbert's last problem......Page 15
1.1 The idea of a proof......Page 17
(a) Natural deduction.......Page 18
(b) The theory of equality.......Page 20
(a) The four parts.......Page 23
(b) Summary of the individual chapters.......Page 24
I Proof systems based on natural deduction......Page 29
(a) Introduction rules as determined by the BHK-conditions.......Page 31
(b) Inversion principle: determination of elimination rules.......Page 32
(c) Discharge principle: definition of derivations.......Page 34
(e) Classical propositional logic.......Page 35
(a) Convertibility.......Page 37
(b) Normal derivations.......Page 39
(c) The subformula structure.......Page 40
(d) The normalization of derivations.......Page 41
(a) Mathematical rules.......Page 43
(b) The subterm property.......Page 45
(a) The rules of equality.......Page 46
(b) Purely syntactic proofs of independence.......Page 48
(a) Replacement rules.......Page 49
Notes to Chapter 2......Page 51
(a) Background to axiomatization.......Page 53
(b) Projective geometry.......Page 56
(c) Lattice theory.......Page 58
3.2 Relational theories and existential axioms......Page 60
Notes to Chapter 3......Page 63
(a) Partial order.......Page 64
(b) Strict partial order.......Page 65
(a) The subterm property.......Page 66
(b) The Whitman conditions.......Page 69
(b) The subterm property.......Page 71
(c) Proof search.......Page 74
(d) Functions.......Page 75
(a) Lattice theory.......Page 76
(b) Strict order with equality.......Page 77
Notes to Chapter 4......Page 81
5.1 Existence in natural deduction......Page 82
(a) Non-triviality in equality.......Page 85
(b) Non-degenerate partial order.......Page 86
(a) The rules of relational lattice theory.......Page 87
(b) Permutability of rules.......Page 89
(c) Derivability of universal formulas.......Page 94
Notes to Chapter 5......Page 96
II Proof systems based on sequent calculus......Page 97
(a) Notation and rules for sequent calculus.......Page 99
(b) `Sequents as sets'.......Page 103
(d) Classical propositional logic.......Page 105
(e) Multisuccedent sequents.......Page 106
(f) Sequent calculi with invertible rules.......Page 107
(a) Cut elimination in the presence of axioms.......Page 111
(b) Four approaches to extension by axioms.......Page 118
6.3 Predicate logic with equality......Page 120
6.4 Herbrand's theorem for universal theories......Page 124
Notes to Chapter 6......Page 125
(a) Minimal derivations.......Page 127
(b) Partial order.......Page 128
(c) Linear order.......Page 131
(d) Extension algorithm from partial to linear order.......Page 132
7.2 The word problem for linear order......Page 133
(b) Linear order.......Page 134
7.3 Linear lattices......Page 137
Notes to Chapter 7......Page 142
III Proof systems for geometric theories......Page 145
(a) The geometric rule scheme.......Page 147
(b) Examples of geometric theories.......Page 148
8.2 Proof theory of geometric theories......Page 152
8.3 Barr's theorem......Page 158
Notes to Chapter 8......Page 159
(a) Finitary basic concepts.......Page 161
(b) Derivations in left and right rule systems.......Page 163
9.2 From geometric to co-geometric axioms and rules......Page 164
9.3 Duality of dependent types and degenerate cases......Page 169
Notes to Chapter 9......Page 170
(a) Basic relations, constructions, and axioms.......Page 171
(b) Multiple-conclusion rules.......Page 172
(c) The rules of projective geometry.......Page 175
(d) The subterm property.......Page 176
10.2 Affine geometry......Page 187
10.3 Examples of proof analysis in geometry......Page 194
Notes to Chapter 10......Page 195
IV Proof systems for non-classical logics......Page 197
11.1 The language and axioms of modal logic......Page 199
11.2 Kripke semantics......Page 201
11.3 Formal Kripke semantics......Page 203
(a) Basic modal logic.......Page 204
(b) Extensions.......Page 205
11.4 Structural properties of modal calculi......Page 207
11.5 Decidability......Page 215
11.6 Modal calculi with equality, undefinability results......Page 224
(a) Soundness.......Page 227
(b) Completeness.......Page 229
Notes to Chapter 11......Page 233
(a) Semantics and syntax of quantified modal logic.......Page 236
(b) Structural properties.......Page 239
(c) Soundness and completeness.......Page 245
12.2 Provability logic......Page 248
12.3 Intermediate logics......Page 253
12.4 Substructural logics......Page 263
Notes to Chapter 12......Page 265
Bibliography......Page 268
Index of names......Page 276
Index of subjects......Page 278