Structural Proof TheoryStructural 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. |
Contents
1 FROM NATURAL DEDUCTION TO SEQUENT CALCULUS | 1 |
2 SEQUENT CALCULUS FOR INTUITIONISTIC LOGIC | 25 |
3 SEQUENT CALCULUS FOR CLASSICAL LOGIC | 47 |
4 THE QUANTIFIERS | 61 |
5 VARIANTS OF SEQUENT CALCULI | 87 |
6 STRUCTURAL PROOF ANALYSIS OF AXIOMATIC THEORIES | 126 |
7 INTERMEDIATE LOGICAL SYSTEMS | 156 |
8 BACK TO NATURAL DEDUCTION | 165 |
SIMPLE TYPE THEORY AND CATEGORIAL GRAMMAR | 219 |
PROOF THEORY AND CONSTRUCTIVE TYPE THEORY | 225 |
PESCA A PROOF EDITOR FOR SEQUENT CALCULUS | 235 |
| 245 | |
AUTHOR INDEX | 251 |
| 253 | |
INDEX OF LOGICAL SYSTEMS | 257 |
DIVERSITY AND UNITY IN STRUCTURAL PROOF THEORY | 211 |
Other editions - View all
Common terms and phrases
A D B admissible antecedent apply arbitrary assume assumptions atoms axiom Chapter classical conclusion conjunction connectives consider consists constructive contain contexts continued contraction conversion corresponding cut elimination cut formula cut-free cut-height defined definition derivation direct discharge disjunction elimination rules equality example excluded middle expressed extension first follows function G3ip Gentzen given gives implication inductive hypothesis inference instances intuitionistic intuitionistic logic inversion language last rule left premiss Lemma logical rules major premiss method multiset natural deduction nonlogical rules normal normal form obtain occurrence open assumptions permuted possible predicate logic present principal produces proof proof search proof theory Prop propositional logic prove quantifier regular relation replaced restriction result right premiss sequent calculus similarly step structural rules substitution Theorem theory thread tion transformed translation tree type theory usual variable weakening