How is it that infinitary methods can be applied to finitary mathematics? Godel's t: a case study

摘要

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 Godel's system T of primitive recursive functionals of finite types by constructing an ε_0-recursive function []_o:T → ω so that a reduces to b implies [a]_o > [b]_o. The construction of []_o is based on a careful analysis of the Howard-Schutte treatment of Godel'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 []_o is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Godel'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 < ω_(n+2)-descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T_O is primitive recursive, thus nay type one functional a in T_O 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 form our finitistic and constructive treatment of the terms of Godel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO(ε_0) ∏_2~0 - Refl(PA) and PRA + PRWO(ω_(n+2)) ∏_2~0 - Refl(IΣ_(n+1)), hence PRA + PRWO(ε_0) Con(PA) and PRA + PRWO(ω_(n+2)) 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.