Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-30T23:16:30.813Z Has data issue: false hasContentIssue false
  • English
  • Français

How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study

Published online by Cambridge University Press:  12 March 2014

Andreas Weiermann
Andreas Weiermann*
Affiliation:
Institut Für Mathematische Logik Und Grundlagenforschung, Der Westfälischen Wilhelms-, Universität Münster, Einsteinstrasse 62, D-48149 Münster, Germany. E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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 ∈ 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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 63 , Issue 4 , December 1998 , pp. 1348 - 1370
Copyright
Copyright © Association for Symbolic Logic 1998

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Aczel, P., Simmons, H., and Wainer, S. S. (editors), Proof theory: a selection of papers from the Leeds proof theory meeting 1990, Cambridge University Press, 1992.Google Scholar
[2] Arai, T., Variations on a theme by Weiermann, to appear in Journal of Symbolic Logic .Google Scholar
[3] Arai, T., Proof theory for theories of ordinals, preprint, 1995.Google Scholar
[4] Arai, T., Proof theory for theories of ordinals I: reflecting ordinals, preprint, 1996.Google Scholar
[5] Arai, T., Systems of ordinal diagrams, preprint, 1996.Google Scholar
[6] Arai, T., Consistency proofs via pointwise induction, Archive for Mathematical Logic, vol. 37 (1998), no. 3, pp. 149—165.Google Scholar
[7] Barendregt, H., The lambda calculus: its syntax and semantics, North-Holland, 1981.Google Scholar
[8] Beckmann, A., Separating systems of bounded arithmetic, Dissertation, Münster, 1996.Google Scholar
[9] Beckmann, A. and Weiermann, A., How to characterize the elementary recursive functions by Howard-Schutte style methods, preprint, submitted, 1996.Google Scholar
[10] Beckmann, A., A term rewriting characterization of the poly time functions and related complexity classes, Archive for Mathematical Logic, vol. 36 (1996), pp. 11—30.Google Scholar
[11] Bellantoni, S. and Cook, S., A new recursion-theoretic characterization of the poly time functions, Computational Complexity, vol. 2 (1992), no. 2, pp. 97—110.Google Scholar
[12] Blankertz, B. and Weiermann, A., How to characterize provably total functions by the Buchholz operator method, Proceedings of Gödel 96, Lecture Notes in Logic, vol. 6, Springer-Verlag, Berlin, 1996, pp. 205—213.Google Scholar
[13] Buchholz, W., The Ωμ+1-rule, in [21], pp. 188—233.Google Scholar
[14] Buchholz, W., Ordinal analysis of ID V , in [21], pp. 234—260.Google Scholar
[15] Buchholz, W., A simplified version of local predicativity, in [1], pp. 115—148.CrossRefGoogle Scholar
[16] Buchholz, W., Three contributions to the conference on recent advances in proof theory, mimeographed, 1980.Google Scholar
[17] Buchholz, W., A new system of proof-theoretic ordinal functions, Annals of Pure and Applied Logic, vol. 32 (1986), pp. 195—207.Google Scholar
[18] Buchholz, W., Notation systems for infinitary derivations, Archive for Mathematical Logic, vol. 30 (1991), no. 5–6, pp. 277—296.Google Scholar
[ 19] Buchholz, W., Proof-theoretic analysis of termination proofs, Annals of Pure and Applied Logic, vol. 75 (1995), pp. 57—65.Google Scholar
[20] Buchholz, W., Cichon, E. A., and Weiermann, A., A uniform approach to fundamental sequences and hierarchies, Mathematical Logic Quarterly, vol. 40 (1994), pp. 273—286.CrossRefGoogle Scholar
[21] Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W. (editors), Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics, vol. 897, Springer-Verlag, Berlin, 1981.Google Scholar
[22] Cichon, E. A., Termination proofs and complexity characterisations, Leeds proof theory 1990 (Aczel, et al., editors), Cambridge University Press, 1992, pp. 173—193.Google Scholar
[23] Cichon, E. A. and Weiermann, A., A termination ordering for primitive recursive schemata, preprint, submitted, 1995.Google Scholar
[24] Cichon, E. A., Term rewriting theory for the primitive recursive functions, Annals of Pure and Applied Logic, vol. 83 (1997), pp. 199—223.CrossRefGoogle Scholar
[25] Feferman, S., How is it that finitary proof theory became infinitary?, Bulletin of Symbolic Logic, vol. 1 (1995), pp. 207—208, abstract.Google Scholar
[26] Friedman, H. and Sheard, M., Elementary descent recursion and proof theory, Annals of Pure and Applied Logic, vol. 71 (1995), pp. 1—45.Google Scholar
[27] Girard, J. Y., Π2 1-logic: Parti: dilators, Annals of Mathematical Logic, vol. 21 (1981), pp. 75—219.Google Scholar
[28] Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialéctica, vol. 12 (1958), pp. 280—287.Google Scholar
[29] Hofbauer, D., Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Proceedings of the 2nd ALP, Lecture Notes in Computer Science, vol. 463, Springer-Verlag, Berlin, 1990, pp. 347—358.Google Scholar
[30] Hofbauer, D., Termination proofs and derivation lengths in term rewriting systems, Forschungsberichte des Fachbereichs Informatik, Bericht 92-46, Technische Universität Berlin, 1991.Google Scholar
[31] Howard, W. A., Assignment of ordinals to terms for primitive recursive functionals of finite type, Intuitionism and proof theory, North-Holland, Amsterdam, 1970, pp. 443—458.Google Scholar
[32] Howard, W. A., A system of abstract constructive ordinals, this Journal, vol. 37 (1972), pp. 353—374.Google Scholar
[33] Howard, W. A., Ordinal analysis of bar recursion of type zero, Compositio Mathematica, vol. 42 (1980), pp. 105—119.Google Scholar
[34] Kreisel, G., On the interpretation of non-finitist proofs II, this Journal, vol. 17 (1952), pp. 43—58.Google Scholar
[35] Leivant, D., Predicative recurrence in finite type, Logical foundations of computer science (Nerode, A. and Matiyasevich, Y. V., editors), Lecture Notes in Computer Science, vol. 813, Springer-Verlag, Berlin, 1994, pp. 227—239.Google Scholar
[36] Leivant, D., Ramified recurrence and computational complexity I: word recurrence and poly-time, Feasible mathematics II (Clote, P. and Remmel, J., editors), Perspectives in Computer Science, Birkhäuser, 1995, pp. 320—343.Google Scholar
[37] Möllerfeld, M. and Weiermann, A., A uniform approach to -≺-recursion, preprint, 1996.Google Scholar
[38] Parsons, C., On a number-theoretic choice schema and its relation to induction, Inflationism and proof theory (Kino, A., Myhill, J., and Vesley, R. E., editors), North-Holland, 1970, pp. 459—473.Google Scholar
[39] Parsons, C., On n-quantifier induction, this Journal, vol. 37 (1972), no. 3, pp. 466—482.Google Scholar
[40] Pohlers, W., Proof-theoretic analysis of ID v by the method of local predicativity, in [21], pp. 261—357.Google Scholar
[41] Pohlers, W., A short course in ordinal analysis, in [1], pp. 27—78.Google Scholar
[42] Pohlers, W., Pure proof theory: aims, methods and results, Bulletin of Symbolic Logic, vol. 2 (1996), no. 2, pp. 159—188.CrossRefGoogle Scholar
[43] Rathjen, M., Fragments of Kripke-Platek set theory with infinity, in [1], pp. 251—273.CrossRefGoogle Scholar
[44] Rathjen, M., An ordinal analysis of Π2 1-comprehension and related systems, preprint.Google Scholar
[45] Rathjen, M., Recent advances in ordinal analysis: Π2 1 – CA and related systems, Bulletin of Symbolic Logic, vol. 1 (1995), no. 4, pp. 468—485.Google Scholar
[46] Rathjen, M. and Weiermann, A., Proof-theoretic investigations on Kruskal's theorem, Annals of Pure and Applied Logic, vol. 60 (1993), pp. 49—88.Google Scholar
[47] Rose, H. E., Subrecursion: functions and hierarchies, Oxford University Press, 1984.Google Scholar
[48] Schmerl, U., Number theory and the Bachmann-Howard ordinal, Proceedings of the Herbrand symposium (Stern, J., editor), North-Holland, Amsterdam, 1981, pp. 287—298.Google Scholar
[49] K. Schütte, , Proof theory, Springer-Verlag, Berlin, 1977.Google Scholar
[50] Schwichtenberg, H., Classifying recursive functions, to appear in Handbook of Recursion Theory .Google Scholar
[51] Schwichtenberg, H., Einige Anwendungen von unendlichen Termen und Wertfunktionalen, Habilitationschrift, Münster, 1973.Google Scholar
[52] Schwichtenberg, H., Elimination of higher type levels in definitions of primitive recursive functionals by means of transfinite recursion, Logic colloquium '73 (Rose, and Sheperdson, , editors), North-Holland, Amsterdam, 1975, pp. 279—303.Google Scholar
[53] Smith, R., The consistency strength of some finite forms of the Higman and Kruskal theorems, Harvey Friedman's research on the foundations of mathematics (Harrington, L. A. et al., editors), North-Holland, Amsterdam, 1985, pp. 119—136.Google Scholar
[54] Stärk, R., The finite stages of inductive definitions, Proceedings of Gödel 96, Lecture Notes in Logic, vol. 6, Springer-Verlag, Berlin, 1996, pp. 267—290.Google Scholar
[55] Takeuti, G., Proof theory, second ed., North-Holland, Amsterdam, 1987.Google Scholar
[56] Troelstra, A. S., Metamathematical investigations ofintuitionistic arithmetic and analysis, ILLC Prepublication Series, vol. X-93-05, 1973, second, corrected edition of Lecture Notes in Mathematics, vol. 344.Google Scholar
[57] Weiermann, A., Rewriting theory for the Hydra battle and the extended Grzegorczyk hierarchy, to appear in Journal of Symbolic Logic .Google Scholar
[58] Weiermann, A., A proof of strongly uniform termination for Gödels T by methods from local predicativity, preprint, to appear in Archive for Mathematical Logic , 1995.Google Scholar
[59] Weiermann, A., Termination proofs for term rewriting systems by lexicographic path orderings yield multiply recursive derivation lengths, Theoretical Computer Science, vol. 139 (1995), pp. 355—362.Google Scholar
[60] Weiermann, A., How to characterize provably total functions by local predicativity, this Journal, vol. 61 (1996), pp. 52—69.Google Scholar
[61] Weiermann, A., Bounding derivation lengths with functions from the slow growing hierarchy, Archive for Mathematical Logic, vol. 37 (1998), pp. 427—441.Google Scholar
[62] Weiermann, A. and Wilken, G., Derivation lengths classifications for -≺-recursive functionals and systems of bar recursion of type 0, in preparation.Google Scholar