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.
Author(s): Helmut Schwichtenberg, Stanley S. Wainer
Series: Perspectives in Logic
Publisher: Cambridge University Press
Year: 2012
Language: English
Commentary: web draft
Pages: 384
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_<ω......Page 194
4. ID_<ω and Π^1_1-CA_0......Page 195
5. An independence result - Kruskal's theorem......Page 200
1. φ-terms, trees and i-sequences......Page 201
6. Notes......Page 205
Part 3. Constructive Logic and Complexity......Page 207
1. Abstract computability via information systems......Page 209
1. Information systems......Page 210
2. Domains with countable basis......Page 212
3. Function spaces......Page 213
4. Algebras and types......Page 218
5. Partial continuous functionals......Page 220
6. Constructors as continuous functions......Page 221
7. Total and cototal ideals in a fintary algebra......Page 223
1. Structural recursion operators and Goedel's T......Page 224
2. Conversion......Page 225
3. Corecursion......Page 228
4. A common extension T^+ of Goedel's T and Plotkin's PCF......Page 230
5. Confluence......Page 231
6. Ideals as denotation of terms......Page 234
7. Preservation of values......Page 239
8. Operational semantics; adequacy......Page 241
1. Stong normalization......Page 244
2. Normalization by evaluation......Page 247
4. Computable functionals......Page 249
2. Rules for pcond, ∃ and valmax......Page 250
3. Plotkin's definability theorem......Page 251
5. Total functionals......Page 255
2. Equality for total functionals......Page 256
3. Dense and separating sets......Page 257
6. Notes......Page 261
1. Brouwer-Heyting-Kolmogorov and Goedel......Page 263
2. Formulas and predicates......Page 264
3. Equalities......Page 266
4. Existence, conjunction and disjunction......Page 268
6. Totality and induction......Page 269
7. Coinductive definitions......Page 272
2. Realizability interpretation......Page 275
1. Decorating → and ∀......Page 276
2. Decorating coinductive definitions......Page 278
3. The type of a formula, realizability and witnesses......Page 279
5. Computational variants of some inductively defined predicates......Page 283
6. Computational variants of totality and induction......Page 285
7. Soundness......Page 286
8. An example: list reversal......Page 290
9. Computational content for coinductive definitions......Page 292
3. Refined A-translation......Page 295
1. Definite and goal formulas......Page 297
2. Extraction from weak existence proofs......Page 300
4. Example: Fibonacci numbers......Page 303
5. Example: well-foundedness of the natural numbers......Page 304
6. Example: the hsh-theorem......Page 308
4. Goedel's Dialectica interpretation......Page 309
1. Positive and negative types......Page 310
2. Goedel translation......Page 311
3. Characterization......Page 312
4. Soundness......Page 314
5. A unified treatment of modified realizability and the Dialectica interpretation......Page 319
6. Dialectica interpretation of general induction......Page 320
5. Optimal decoration of proofs......Page 321
1. Decoration algorithm......Page 322
2. List reversal, again......Page 325
3. Passing continuations......Page 328
1. Informal proof......Page 329
2. Extracted terms......Page 330
7. Notes......Page 332
8. Linear Two-Sorted Arithmetic......Page 335
1. Provable recursion and complecity in EA(;)......Page 336
1. The theory EA(;)......Page 337
2. Elementary functions are provably recursive......Page 338
3. Provably recursive functions are elementary......Page 341
2. A two-sorted variant T(;) of Goedel's T......Page 342
1. Higher order terms with input / output restrictions......Page 343
2. Examples......Page 344
3. Elementary functions are definable......Page 345
4. Definable functions are elementary......Page 347
1. LT(;)-terms......Page 350
2. Examples......Page 351
4. LT(;)-definable functions are polynomial time......Page 353
5. The first-order fragment T_1(;) of T(;)......Page 357
1. Motivation......Page 359
2. LA(;)-proof terms......Page 360
3. LA(;) and its provably recursive functions......Page 362
5. Application: Insertion sort in LA(;)......Page 363
5. Notes......Page 365
Bibliography......Page 367
Index......Page 379
