PREFACE
INTRODUCTION
Structural Proof Theory
Use of this book in theaching
What is new in this book?
1. FROM NATURAL DEDUCTION TO SEQUENT CALCULUS
1.1. Logical systems
1.2. Natural deduction
1.3. From natural deduction to sequent calculus
1.4. The structure of proofs
Notes to Chapter 1
2. SEQUENT CALCULUS FOR INTUITIONISTIC LOGIC
2.1. Constructive reasoning
2.2. Intuitionistic sequent calculus
2.3. Proof methods for admissibility
2.4. Admissibility of contraction and cut
2.5. Some consequences of cut elimination
Notes to Chapter 2
3. SEQUENT CALCULUS FOR CLASSICAL LOGIC
3.1. An invertible classical calculus
3.2. Admissibility of structural rules
3.3. Completeness
Notes to Chapter 3
4. THE QUANTIFIERS
4.1. Quantifiers in natural deduction and in sequent calculus
4.2. Admissibility of structural rules
4.3. Applications of cut elimination
4.4. Completeness of classical predicate logic
Notes to Chapter 4
5. VARIANTS OF SEQUENT CALCULI
5.1. Sequent calculi with independent contexts
5.2. Sequent calculi in natural deduction style
5.3. An intuitionistic multisuccedent calculus
5.4. A classical single-succedent calculus
5.5. A terminating intuitionistic calculus
Notes to Chapter 5
6. STRUCTURAL PROOF ANALYSIS OF AXIOMATIC THEORIES
6.1. From axioms to rules
6.2. Admissibility of structural rules
6.3. Four approaches to extension by axioms
6.4. Properties of cut-free derivations
6.5. Predicate logic with equality
6.6. Application to axiomatic systems
Notes to Chapter 6
7. INTERMEDIATE LOGICAL SYSTEMS
7.1. Sequent calculi with the weak law of exCluded middle
7.2. A sequent calculus for stable logic
7.3. Sequent calculi for Dummett logic
Notes to Chapter 7
8. BACK TO NATURAL DEDUCTION
8.1. Natural deduction with general elimination rules
8.2. Translation from sequent calculus to natural deduction
8.3. Translation from natural deduction to sequent calculus
8.4. Derivations with cuts and non-normal derivations
8.5. The structure of normal derivations
8.6. Classical natural deduction for propositional logic
Notes to Chapter 8
CONCLUSION: DIVERSITY AND UNITY IN STRUCTURAL PROOF THEORY
Comparing sequent calculus and natural deduction
A uniform logical calculus
APPENDIX A: SIMPLE TYPE THEORY AND CATEGORIAL GRAMMAR
A.1. Simple type theory
A.2. Categorial grammar for logical languages
Notes to Appendix A
Appendix B: Proof theory and constructive type theory
B.1. Lower-level type theory
B.2. Higher-level type theory
B.3. Type systems
Notes to Appendix B
Appendix C: A proof editor for sequent calculus
C.1. Introduction
C.2. Two sample sessions
C.3. Some commands
C.4. Axiom files
C.5. On the implementation
Notes to Appendix C
Electronic references
BIBLIOGRAPHY
AUTHOR INDEX
SUBJECT IDEX
INDEX OF LOGICAL SYSTEMS