AbstractInspired 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 Tn 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 Tn.) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the Tn-derivation lengths in terms of ω+2-descent recursive functions. The derivation lengths of type one functionals from Tn (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 ∈ T0 is primitive recursive, thus any type one functional a in T0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T1 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(ε0) ⊢ Π20 − Refl(PA) and PRA + PRWO(ωn+2) ⊢ Π20 − 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.
The name for Kojman–Shelah collapsing function
