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

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### 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 antecedent apply atomic formulas axiom or conclusion categorial grammar classical logic classical propositional logic conclusion of LJ conjunction corresponding cut elimination cut formula cut-free deﬁned deﬁnition derivable in G3ip discharge disjunction E|xA elimination rules ElxA excluded middle F Q A F Q C ﬁnd ﬁrst follows function G3cp G3im Gem-at Gentzen gives a derivation Harrop formulas height of derivation height-preserving implication inductive hypothesis instances introduction rules intuitionistic logic inversion last rule left premiss left rule Lemma logical rules major premiss multiset multiset reduct multisuccedent natural deduction derivation nonlogical rules normal form obtain open assumptions permuted predicate logic premiss of cut principal formula proof search propositional logic quantiﬁer rules regular sequents right premiss root-ﬁrst rule of excluded rules of inference Section sequent calculus derivations single succedent structural proof theory structural rules subformula property substitution Theorem transformed translation type theory weakening and contraction weakening or contraction