Proofs and Computations

Description

Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central role and are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Π11-CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic. Preface......Page 3 Preliminaries......Page 7 Contents......Page 9 Part 1. Basic Proof Theory & Computability......Page 11 1. Logic......Page 13 1. Terms and formulas......Page 14 3. Subformulas......Page 15 4. Examples of derivations......Page 16 5. Introduction and elimination rules for → and ∀......Page 17 6. Properties of negation......Page 18 7. Introduction and elimination rules for ∨, ∧ and ∃......Page 19 8. Intuitionistic and classical derivability......Page 20 9. Godel-Gentzen translation......Page 24 2. Normalization......Page 25 1. Conventions......Page 26 2. Permutative conversions......Page 28 3. Simplification conversions......Page 29 4. Strong normalization......Page 30 5. On disjunction......Page 34 6. The structure of normal derivations......Page 35 1. Tree models......Page 38 3. Soundness......Page 40 4. Counter models......Page 41 5. Completeness......Page 43 1. Models......Page 46 2. Soundness of classical logic......Page 47 3. Completeness of classical logic......Page 48 5. Tait calculus......Page 50 6. Notes......Page 51 1. Programs......Page 53 2. Program constructs......Page 54 3. Register machine computable functions......Page 55 1. Defintion and simple properties......Page 56 3. The class E......Page 58 4. Closure properties of E......Page 60 5. Coding finite lists......Page 61 1. Program numbers......Page 64 2. Normal form......Page 65 3. Σ^0_1-definable relations and μ-recursive functions......Page 66 4. Computable functions......Page 67 1. Least fixed points of recursive definitions......Page 68 2. The principles of finite support and monotonicity; the effective index property......Page 69 3. Recursion theorem......Page 70 4. Recursive programs and partial recursive functions......Page 71 1. Primitive recursive functions......Page 72 2. Loop-programs......Page 73 3. Reduction to primitive recursion......Page 74 4. A complexity hierarchy for Prim......Page 75 2. Characterization of Σ^0_1-definable and recursive relations......Page 78 3. Arithmetical relations......Page 79 5. Universal Σ^0_{r+1}-definable relations......Page 80 6. Σ^0_r-complete relations......Page 81 1. Analytical relations......Page 82 2. Closure properties......Page 83 3. Universal Σ^1_{r+1}-definable relations......Page 84 2. Ordinal assignments; recursive ordinals......Page 85 3. A hierarchy of total recursive functionals......Page 86 1. Monotone operators......Page 88 3. Approximation of the least and greatest fixed point......Page 89 4. Continuous operators......Page 91 5. The accessible part of a relation......Page 92 7. Definability of least fixed points for monotone operators......Page 93 8. Some counterexamples......Page 94 10. Notes......Page 96 3. Godel's Theorems......Page 97 1. Basic arithmetic in IΔ_0(exp)......Page 98 2. Provable recursion in IΔ_0(exp)......Page 100 3. Proof theoretic characterization......Page 103 1. Godel numbers of terms, formulas and derivations......Page 106 2. Elementary functions on Godel numbers......Page 108 3. Axiomatized theories......Page 111 4. Undefinability of the notion of truth......Page 112 1. Representable relations and functions......Page 113 2. Undefinability of the notion of truth in formal theories......Page 114 2. Incompleteness......Page 115 1. Weak arithmetical theories......Page 117 2. Robinson's theory Q......Page 119 3. Σ_1 formulas......Page 120 1. Formalized Σ_1-completeness......Page 121 2. Derivability conditions......Page 123 7. Notes......Page 124 Part 2. Provable Recursion in Classical Systems......Page 125 4. The Provably Recursive Functions of Arithmetic......Page 127 1. Primitive recursion and IΣ_1......Page 129 2. ε_0-recursion in Peano Arithmetic......Page 133 1. Ordinals below ε_0......Page 134 2. The fast growing hierarchy and ε_0-recursion......Page 137 3. Provable recursiveness of H_α and F_α......Page 142 1. The infinitary system......Page 148 2. Embedding of PA......Page 151 3. Cut elimination......Page 153 4. The classification theorem......Page 157 1. Goodstein sequences......Page 158 2. The modified finite Ramsey theorem......Page 160 5. Notes......Page 164 1. The subrecursive stumblingblock......Page 165 2. Accessible recursive functions......Page 169 1. Structured tree ordinals......Page 171 2. Collapsing properties of G......Page 174 3. The accessible recursive functions......Page 181 1. Finitely iterated inductive definitions......Page 182 2. The infinitary system ID_k(W)^∞......Page 185 3. Ordinal analysis of ID_k......Page 190 4. Accessible = provable recursive in ID_