Structural proof theory

Main subject categories: • Structural proof theory • Structural proof analysis • Proof theory • Logical systems • Mathematical logicStructural 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. The book contains a wealth of results on proof-theoretical systems, including extensions of such systems from logic to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. 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 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. The Book Contains A Wealth Of New Results On Proof-theoretical Systems, Including Extensions Of Such Systems From Logic To Mathematics, And On The Connection Between The Two Main Forms Of Structural Proof Theory - Natural Deduction And Sequent Calculus. The Authors Emphasize The Computational Context Of Logical Results. A Special Feature Of The Volume Is A Computerized System For Developing Proofs Interactively, Downloadable From The Web And Regularly Updated.--jacket. 1. From Natural Deduction To Sequent Calculus -- 2. Sequent Calculus For Intuitionistic Logic -- 3. Sequent Calculus For Classical Logic -- 4. The Quantifiers -- 5. Variants Of Sequent Calculi -- 6. Structural Proof Analysis Of Axiomatic Theories -- 7. Intermediate Logical Systems -- 8. Back To Natural Deduction -- Conclusion: Diversity And Unity In Structural Proof Theory -- App. A. Simple Type Theory And Categorical Grammar -- App. B. Proof Theory And Constructive Type Theory -- App. C. Pesca -- A Proof Editor For Sequent Calculus / Aarne Ranta. Sara Negri, Jan Von Plato ; With An Appendix By Aarne Ranta. Includes Bibliographical References (p. 245-249) And Indexes. Structural proof theory studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to structural proof theory and a work of research that will be of interest to specialists. A special feature is a downloadable computer program for developing proofs interactively.

a Concise Introduction To Structural Proof Theory, A Branch Of Logic Studying The General Structure Of Logical And Mathematical Proofs.