Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics, and computer science. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated.
Author(s): Professor Sara Negri, Jan von Plato, Aarne Ranta
Publisher: CUP
Year: 2001
Language: English
Pages: 276
About ......Page 1
Title ......Page 3
Copyright ......Page 4
Contents ......Page 5
Preface ......Page 9
Introduction ......Page 11
1.1. Logical systems ......Page 19
1.2. Natural deduction ......Page 23
1.3. From natural deduction to sequent calculus ......Page 31
1.4. The structure of proofs ......Page 38
Notes to Chapter 1 ......Page 41
2.1. Constructive reasoning ......Page 43
2.2. Intuitionistic sequent calculus ......Page 46
2.3. Proof methods for admissibility ......Page 48
2.4. Admissibility of contraction and cut ......Page 51
2.5. Some consequences of cut elimination ......Page 58
Notes to Chapter 2 ......Page 64
3. SEQUENT CALCULUS FOR CLASSICAL LOGIC ......Page 65
3.1. An invertible classical calculus ......Page 66
3.2. Admissibility of structural rules ......Page 71
3.3. Completeness ......Page 76
Notes to Chapter 3 ......Page 78
4.1. Quantifiers in natural deduction and in sequent calculus ......Page 79
4.2. Admissibility of structural rules ......Page 88
4.3. Applications of cut elimination ......Page 94
4.4. Completeness of classical predicate logic ......Page 99
Notes to Chapter 4 ......Page 104
5.1. Sequent calculi with independent contexts ......Page 105
5.2. Sequent calculi in natural deduction style ......Page 116
5.3. An intuitionistic multisuccedent calculus ......Page 126
5.4. A classical single succedent calculus ......Page 132
5.5. A terminating intuitionistic calculus ......Page 140
Notes to Chapter 5 ......Page 142
6.1. From axioms to rules ......Page 144
6.2. Admissibility of structural rules ......Page 149
6.3. Four approaches to extension by axioms ......Page 152
6.4. Properties of cut-free derivations ......Page 154
6.5. Predicate logic with equality ......Page 156
6.6. Application to axiomatic systems ......Page 159
Notes to Chapter 6 ......Page 172
7. INTERMEDIATE LOGICAL SYSTEMS ......Page 174
7.1. A sequent calculus for the weak law of excluded middle ......Page 175
7.2. A sequent calculus for stable logic ......Page 176
7.3. Sequent calculi for Dummett logic ......Page 178
Notes to Chapter 7 ......Page 182
8. BACK TO NATURAL DEDUCTION ......Page 183
8.1. Natural deduction with general elimination rules ......Page 184
8.2. Translation from sequent calculus to natural deduction ......Page 190
8.3. Translation from natural deduction to sequent calculus ......Page 197
8.4. Derivations with cuts and non-normal derivations ......Page 203
8.5. The structure of normal derivations ......Page 207
8.6. Classical natural deduction for propositional logic ......Page 220
Notes to Chapter 8 ......Page 226
Comparing sequent calculus and natural deduction ......Page 229
A uniform logical calculus ......Page 231
A.1. Simple type theory ......Page 237
A.2. Categorial grammar for logical languages ......Page 239
Notes to Appendix A ......Page 242
B.1. Lower-level type theory ......Page 243
B.2. Higher-level type theory ......Page 248
B.3. Type systems ......Page 250
Notes to Appendix B ......Page 252
C.1. Introduction ......Page 253
C.2. Two example sessions ......Page 254
C.3. Some commands ......Page 257
C.4. Axiom files ......Page 259
C.5. On the implementation ......Page 260
Electronic references ......Page 261
BIBLIOGRAPHY ......Page 263
AUTHOR INDEX ......Page 269
SUBJECT INDEX ......Page 271
INDEX OF LOGICAL SYSTEMS ......Page 275
