How is it that infinitary methods can be applied to finitary mathematics? Gödel's t: A case study
Journal of Symbolic Logic 63 (4):1348-1370 (1998)
| Abstract | Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε 0 -recursive function [] 0 : T → ω so that a reduces to b implies [a] $_0 > [b]_0$ . The construction of [] 0 is based on a careful analysis of the Howard-Schütte treatment of Gödel's T and utilizes the collapsing function ψ: ε 0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [] 0 is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Gödel's T by the method of local predicativity" by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper. Indeed, for given n let T n be the subsystem of T in which the recursors have type level less than or equal to n+2. (By definition, case distinction functionals for every type are also contained in T n .) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the T n -derivation lengths in terms of ω n+2 -descent recursive functions. The derivation lengths of type one functionals from T n (hence also their computational complexities) are classified optimally in terms of $ -descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T 0 is primitive recursive, thus any type one functional a in T 0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T 1 in terms of multiple recursion. As proof-theoretic corollaries we reobtain the classification of the IΣ n+1 -provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO ( $\varepsilon_0) \vdash \Pi^0_2$ - Refl(PA) and PRA + PRWO ( $\omega_{n+2}) \vdash \Pi^0_2$ - Refl(I Σ n+1 ), hence PRA + PRWO( $\epsilon_0) \vdash$ Con(PA) and PRA + PRWO( $\omega_{n+2}) \vdash$ Con(IΣ n+1 ). For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,679 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesMichael Rathjen (1992). A Proof-Theoretic Characterization of the Primitive Recursive Set Functions. Journal of Symbolic Logic 57 (3):954-969.
Kurt Gödel (1980). On a Hitherto Unexploited Extension of the Finitary Standpoint. Journal of Philosophical Logic 9 (2):133 - 142.
Andreas Weiermann (2001). Some Interesting Connections Between the Slow Growing Hierarchy and the Ackermann Function. Journal of Symbolic Logic 66 (2):609-628.
Samuel R. Buss (1994). On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedup for Arithmetics. Journal of Symbolic Logic 59 (3):737-756.
Zlatan Damnjanovic (1995). Minimal Realizability of Intuitionistic Arithmetic and Elementary Analysis. Journal of Symbolic Logic 60 (4):1208-1241.
G. Longo & E. Moggi (1984). The Hereditary Partial Effective Functionals and Recursion Theory in Higher Types. Journal of Symbolic Logic 49 (4):1319-1332.
Robert A. Di Paola (1981). A Lift of a Theorem of Friedberg: A Banach-Mazur Functional That Coincides with No Α-Recursive Functional on the Class of Α-Recursive Functions. Journal of Symbolic Logic 46 (2):216 - 232.
Markus Michelbrink (2006). A Buchholz Derivation System for the Ordinal Analysis of KP + Π₃-Reflection. Journal of Symbolic Logic 71 (4):1237 - 1283.
Thomas Strahm (2002). Review: Andreas Weiermann, How Is It That Infinitary Methods Can Be Applied to Finitary Mathematics? Gödel's T: A Case Study. [REVIEW] Bulletin of Symbolic Logic 8 (3):435-436.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads6 ( #145,615 of 549,078 )Recent downloads (6 months)1 ( #63,317 of 549,078 )How can I increase my downloads? |
My notes
Discussion
