Handbook of Proof TheoryS.R. Buss This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that the two introductory articles come first; these are then followed by articles from core classical areas of proof theory; the handbook concludes with articles that deal with topics closely related to computer science. |
Contents
| 79 | |
Chapter III Hierarchies of Provably Recursive Functions | 149 |
Chapter IV Subsystems of Set Theory and Second Order Number Theory | 209 |
Chapter V Gödels Functional Dialectica Interpretation | 337 |
Chapter VI Realizability | 407 |
Chapter VII The Logic of Provability | 475 |
| 547 | |
| 639 | |
Chapter X Types in Logic Mathematics and Programming | 683 |
| 787 | |
| 797 | |
Common terms and phrases
analysis apply assignment assume axiomatized boolean bounded arithmetic Buss classical clauses completeness Computer Science consider consistent constructive contains Corollary cut elimination cut-free defined denote derivation disjunction equality equivalent example expression Feferman finite first-order first-order logic formal free variables free-cut Frege Frege systems function symbols Gödel Hence hierarchy implies incompleteness theorem induction hypothesis inductive definitions inference interpretation intuitionistic intuitionistic logic iterated Journal of Symbolic language Lemma logic program lower bounds modal modus ponens natural numbers notation notion Nuprl obtain occurs operator ordinal ordinal analysis Peano arithmetic polynomial predicate primitive recursive functions proof system proof theory proof-theoretic propositional logic propositional proof provability logic provably recursive prove Pudlák quantifier-free quantifiers realizability relation symbols resolution rules semantics sentences sequent calculus set theory structure subformula substitution Suppose Symbolic Logic tautology transfinite translation Troelstra true type theory valid X'-formula