Structural Proof Theory

Contents......Page 6
Preface......Page 10
Introduction......Page 12
1.1. Logical systems......Page 20
1.2. Natural deduction......Page 24
1.3. From natural deduction to sequent calculus......Page 32
1.4. The structure of proofs......Page 39
Notes to Chapter 1......Page 42
2.1. Constructive reasoning......Page 44
2.2. Intuitionistic sequent calculus......Page 47
2.3. Proof methods for admissibility......Page 49
2.4. Admissibility of contraction and cut......Page 52
2.5. Some consequences of cut elimination......Page 59
Notes to Chapter 2......Page 65
3. Sequent Calculus for Classical Logic......Page 66
3.1. An invertible classical calculus......Page 67
3.2. Admissibility of structural rules......Page 72
3.3. Completeness......Page 77
Notes to Chapter 3......Page 79
4.1. Quantifiers in natural deduction and in sequent calculus......Page 80
4.2. Admissibility of structural rules......Page 89
4.3. Applications of cut elimination......Page 95
4.4. Completeness of classical predicate logic......Page 100
Notes to Chapter 4......Page 105
5.1. Sequent calculi with independent contexts......Page 106
5.2. Sequent calculi in natural deduction style......Page 117
5.3. An intuitionistic multisuccedent calculus......Page 127
5.4. A classical single succedent calculus......Page 133
5.5. A terminating intuitionistic calculus......Page 141
Notes to Chapter 5......Page 143
6.1. From axioms to rules......Page 145
6.2. Admissibility of structural rules......Page 150
6.3. Four approaches to extension by axioms......Page 153
6.4. Properties of cut-free derivations......Page 155
6.5. Predicate logic with equality......Page 157
6.6. Application to axiomatic systems......Page 160
Notes to Chapter 6......Page 173
7. Intermediate Logical Systems......Page 175
7.1. A sequent calculus for the weak law of excluded middle......Page 176
7.2. A sequent calculus for stable logic......Page 177
7.3. Sequent calculi for Dummett logic......Page 179
Notes to Chapter 7......Page 183
8. Back to Natural Deduction......Page 184
8.1. Natural deduction with general elimination rules......Page 185
8.2. Translation from sequent calculus to natural deduction......Page 191
8.3. Translation from natural deduction to sequent calculus......Page 198
8.4. Derivations with cuts and non-normal derivations......Page 204
8.5. The structure of normal derivations......Page 208
8.6. Classical natural deduction for propositional logic......Page 221
Notes to Chapter 8......Page 227
Comparing sequent calculus and natural deduction......Page 230
A uniform logical calculus......Page 232
A.1. Simple type theory......Page 238
A.2. Categorial grammar for logical languages......Page 240
Notes to Appendix A......Page 243
B.1. Lower-level type theory......Page 244
B.2. Higher-level type theory......Page 249
B.3. Type systems......Page 251
Notes to Appendix B......Page 253
C.1. Introduction......Page 254
C.2. Two example sessions......Page 255
C.3. Some commands......Page 258
C.4. Axiom files......Page 260
C.5. On the implementation......Page 261
Electronic references......Page 262
Bibliography......Page 264
Author Index......Page 270
Subject Index......Page 272
Index of Logical Systems......Page 276