Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-19T22:53:26.275Z Has data issue: false hasContentIssue false

How to characterize provably total functions by local predicativity

Published online by Cambridge University Press:  12 March 2014

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]

Abstract

Inspired by Pohlers' proof-theoretic analysis of KPω we give a straightforward non-metamathematical proof of the (well-known) classification of the provably total functions of PA, PA + TI(⊰ ↾) (where it is assumed that the well-ordering ⊰ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1996

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

[1994]Blankertz, B. and Weiermann, A., A uniform approach for characterizing the provably total number-theoretic functions of KPM and (some of) its subsystems, preprint (submitted).Google Scholar
[1994]Buchholz, W., Notation systems for infinitary derivations, Archive for Mathematical Logic, vol. 30, no. 5/6, pp. 277296.CrossRefGoogle Scholar
[1992]Buchholz, W., A simplified version of local predicativity, Proof theory, Leeds 1990 (Aczel, P., Simmons, H., and Wainer, S., editors), Cambridge University Press, pp. 115147.Google Scholar
[1994]Buchholz, W., Cichon, A., and Weiermann, A., A uniform approach to fundamental sequences and subrecursive hierarchies, Mathematical Logic Quarterly, vol. 40, pp. 273286.CrossRefGoogle Scholar
[1987]Buchholz, W. and Wainer, S., Provably computable functions and the fast growing hierarchy, Contemporary Mathematics, vol. 65, pp. 179198.CrossRefGoogle Scholar
[1995]Burr, W., Verschiedene Charakterisierungen der beweisbar rekursiven Funktionen von IEn+1, Master's thesis, Münster.Google Scholar
[1993]Friedman, H. and Sheard, M., Elementary descent recursion and proof theory, Annals of Pure and Applied Logic, vol. 71, no. 1, pp. 145.CrossRefGoogle Scholar
[1989]Pohlers, W., Proof theory, an introduction, vol. 1407, Springer Lecture Notes in Mathematics.Google Scholar
[1991]Pohlers, W., Proof theory and ordinal analysis, Archive for Mathematical Logic, vol. 30, no. 5/6, pp. 311376.CrossRefGoogle Scholar
[1992]Pohlers, W., A short course in ordinal analysis, Proof theory, Leeds 1990 (Aczel, P., Simmons, H., and Wainer, S., editors), Cambridge University Press, pp. 115147.Google Scholar
[1992]Rathjen, M., Fragments of Kripke-Platek set theory with infinity, Proof theory, Leeds 1990 (Aczel, P., Simmons, H., and Wainer, S., editors), Cambridge University Press, pp. 251273.Google Scholar
[1991]Rathjen, M., Proof-theoretic analysis of KPM, Archive for Mathematical Logic, vol. 30, no. 5/6, pp. 377403.CrossRefGoogle Scholar
[1984]Rose, H. E., Subrecursion: Functions and hierarchies, Oxford University Press.Google Scholar
[1977]Schütte, K., Proof theory, Springer-Verlag.Google Scholar
[1971]Schwichtenberg, H., Eine Klassifikation der ε0-rekursiven Funktionen, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 17, pp. 6174.CrossRefGoogle Scholar
[1985]Sieg, W., Fragments of arithmetic, Annals of Pure and Applied Logic, vol. 28, pp. 3371.CrossRefGoogle Scholar
[1987]Takeuti, G., Proof theory, second ed., North-Holland.Google Scholar
[1970]Wainer, S. S., A classification of the ordinal recursive functions, Archiv für Mathematische Logik und Grundlagenforschung, vol. 13, pp. 136–53.CrossRefGoogle Scholar
[1972]Wainer, S. S., Ordinal recursion and a refinement of the ordinal recursive functions, this Journal, vol. 37, pp. 281292.Google Scholar
[1990]Weiermann, A., Ein neuer Zugang zu Kollabierungsfunktionen, Dissertation, Münster.Google Scholar
[ 1991 ]Weiermann, A., Vereinfachte Kollabierungsfunktionen und ihre Anwendungen, Archive for Mathematical Logic, vol. 31, pp. 8594.CrossRefGoogle Scholar