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 epsilon(0)-recursive function [ ](0): T --> omega so that a reduces to b implies [a](0) > [b](0). The construction of [ ](0) is based on a careful analysis of the Howard-Schutte treatment of Godel's T and utilizes the collapsing function psi: epsilon(0) --> omega 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 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 an 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 omega(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 < omega(n+2)-descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one Functional a is an element of 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 Sigma(n=1)-provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Godel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO(epsilon(0)) proves Pi(2)(0) - Refl(PA) and PRA + PRWO(omega(n+2)) proves Pi(2)(0) - Refl(I Sigma(n+1)), hence PRA + PRWO(epsilon(0)) proves Con(PA) and PRA + PRWO(omega(n+2)) proves Con(I Sigma(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.