caa a22 4500 388038985 CHVBK 20180307125015.0 cr unu---uuuuu 161130e199812 xx s 000 0 eng 10.2307/2586654 doi S0022481200014298 pii (NATIONALLICENCE)cambridge-10.2307/2586654 Weiermann Andreas Institut Für Mathematische Logik Und Grundlagenforschung, Der Westfälischen Wilhelms-, Universität Münster, Einsteinstrasse 62, D-48149 Münster, Germany. E-mail: weierma@math.uni-muenster.de How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study [Elektronische Daten] [Andreas Weiermann] 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 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 ∈ 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(ε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. Copyright © Association for Symbolic Logic 1998 The Journal of Symbolic Logic Cambridge University Press 63/4(1998-12), 1348-1370 0022-4812 63:4<1348 1998 63 JSL https://doi.org/10.2307/2586654 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.2307/2586654 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Weiermann Andreas Institut Für Mathematische Logik Und Grundlagenforschung, Der Westfälischen Wilhelms-, Universität Münster, Einsteinstrasse 62, D-48149 Münster, Germany. E-mail: weierma@math.uni-muenster.de NATIONALLICENCE 773 0- The Journal of Symbolic Logic Cambridge University Press 63/4(1998-12), 1348-1370 0022-4812 63:4<1348 1998 63 JSL CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-cambridge