Handbook of Proof Theory

Description

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. Preface......Page 6 Contents......Page 10 I. An Introduction to Proof Theory - Buss......Page 12 1. Proof theory of propositional logic......Page 14 1. Frege proof systems......Page 16 2. The propositional sequent calculus......Page 21 3. Propositional resolution refutations......Page 29 1. Syntax and semantics......Page 37 2. Hilbert-style proof systems......Page 40 3. The first-order sequent calculus......Page 42 4. Cut elimination......Page 47 5. Herbrand's theorem, interpolation and definability theorems......Page 59 6. First-order logic and resolution refutations......Page 70 1. Intuitionistic logic......Page 75 2. Linear logic......Page 81 References......Page 85 II. First-Order Proof Theory of Arithmetic - Buss......Page 90 1. Fragments of arithmetic......Page 92 1. Very weak fragments of arithmetic......Page 93 2. Strong fragments of arithmetic......Page 94 3. Fragments of bounded arithmetic......Page 108 4. Sequent calculus formulations of arithmetic......Page 120 2. Gödel incompleteness......Page 123 1. Arithmetization of metamathematics......Page 124 2. The Gödel incompleteness theorems......Page 129 1. Witnessing theorems......Page 133 2. Witnessing theorem for S^i_2......Page 138 3. Witnessing theorems and conservation results for T^i_2......Page 141 4. Relationships between BΣ_n and IΣ_n......Page 145 1.......Page 148 2.......Page 149 3. A theorem of Wilkie and Paris......Page 150 References......Page 154 III. Hierarchies of Provably Recursive Functions - Fairtlough & Wainer......Page 160 1. Introduction......Page 161 2. Structured ordinals and associated hierarchies......Page 164 3. Complete ω-arithmetic......Page 175 4. Provably recursive functions of PA......Page 186 5. Independence results for PA......Page 201 6. The "true" ordinal of PA......Page 204 7. Theories with transfinite induction......Page 210 References......Page 214 IV. Subsystems of Set Theory and Second Order Number Theory - Pohlers......Page 220 1. Ordinals......Page 221 2. Partial models for axiom systems of set theory......Page 226 3. Connections to subsystems of second order number theory......Page 230 4. Methods......Page 241 1. Peano arithmetic......Page 242 2. An upper bound for spec_{Π^1_1}(NT)......Page 243 3. Lower bounds for spec_{Π^1_1}(NT)......Page 248 4. Computational complexity of Π^0_2-sentences......Page 252 5. Computational complexity of Π^0_2-sentences revisited......Page 264 1. The theories NT_< and their Π^0_2-spectra......Page 272 2. Significance of the theories NT_