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. 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 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.