How is It That Infinitary Methods can be Applied to Finitary Mathematics? Godel's T: A Case Study
Weiermann, Andreas
J. Symbolic Logic, Tome 63 (1998) no. 1, p. 1348-1370 / Harvested from Project Euclid
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 $\varepsilon_0$-recursive function [ ]$_0$: T $\rightarrow \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: \varepsilon_0 \rightarrow \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 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 $\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 $\in 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 ($\varepsilon_0) \vdash \Pi^0_2$ - Refl(PA) and PRA + PRWO ($\omega_{n+2}) \vdash \Pi^0_2$ - Refl(I $\Sigma_{n+1}$), hence PRA + PRWO($\epsilon_0) \vdash$ Con(PA) and PRA + PRWO($\omega_{n+2}) \vdash$ 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.
Publié le : 1998-12-14
Classification: 
@article{1183745635,
     author = {Weiermann, Andreas},
     title = {How is It That Infinitary Methods can be Applied to Finitary Mathematics? Godel's T: A Case Study},
     journal = {J. Symbolic Logic},
     volume = {63},
     number = {1},
     year = {1998},
     pages = { 1348-1370},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745635}
}
Weiermann, Andreas. How is It That Infinitary Methods can be Applied to Finitary Mathematics? Godel's T: A Case Study. J. Symbolic Logic, Tome 63 (1998) no. 1, pp.  1348-1370. http://gdmltest.u-ga.fr/item/1183745635/