Hostname: page-component-cd9895bd7-gvvz8 Total loading time: 0 Render date: 2024-12-23T03:09:41.906Z Has data issue: false hasContentIssue false
  • English
  • Français

Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory

Published online by Cambridge University Press:  12 March 2014

Gerhard Jäger  and
Thomas Strahm
Gerhard Jäger
Affiliation:
Institut für Informatik und Angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland, E-mail: {jaeger,strahm}@iam.unibe.ch
Thomas Strahm
Affiliation:
Institut für Informatik und Angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland, E-mail: {jaeger,strahm}@iam.unibe.ch
Get access Rights & Permissions [Opens in a new window]

Abstract

In this article we introduce systems for metapredicative Mahlo in explicit mathematics and admissible set theory. The exact upper proof-theoretic bounds of these systems are established.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 66 , Issue 2 , June 2001 , pp. 935 - 958
Copyright
Copyright © Association for Symbolic Logic 2001

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]Beckmann, A., Separating fragments of bounded arithmetic, Ph.D. thesis, Universität Münster, 1996.Google Scholar
[2]Beeson, M. J., Foundations of constructive mathematics: Metamathematical studies, Springer, Berlin, 1985.CrossRefGoogle Scholar
[3]Feferman, S., Constructive theories of functions and classes, Logic Colloquium '78 (Boffa, M., van Dalen, D., and McAloon, K., editors). North-Holland, Amsterdam, 1979, pp. 159–224.Google Scholar
[4]Feferman, S. and Jäger, G., Systems of explicit mathematics with non-constructive μ-operator. Part II, Annals of Pure and Applied Logic, vol. 79 (1996), no. 1, pp. 37–52.CrossRefGoogle Scholar
[5]Jäger, G., Die konstruktihle Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Analysis, Ph.D. thesis, UniversitÄt München, 1979.Google Scholar
[6]Jäger, G., A well-ordering proof for Feferman's theory T0, Archiv für mathematische Logik und Grundlagenforschung, vol. 23 (1983), pp. 65–77.CrossRefGoogle Scholar
[7]Jäger, G., The strength of admissibility without foundation, this Journal, vol. 49 (1984), no. 3, pp. 867–879.Google Scholar
[8]Jäger, G., Kahle, R., Setzer, A., and Strahm, T., The proof-theoretic analysis of transfinitely iterated fixed point theories, this Journal, vol. 64 (1999), no. 1, pp. 53–67.Google Scholar
[9]Jäger, G., Kahle, R., and Studer, T., Universes in explicit mathematics, Annals of Pure and Applied Logic, to appear.Google Scholar
[10]Jäger, G. and Pohlers, W., Eine beweistheoretische Untersuchung von und verwandter Systeme, Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse, 1982, pp. 1–28.Google Scholar
[11]Jäger, G. and Strahm, T., Fixed point theories and dependent choice, Archive for Mathematical Logic, vol. 39 (2000), pp. 493–508.Google Scholar
[12]Jäger, G. and Studer, T., Extending the system T0 of explicit mathematics: the limit and Mahlo axioms, Annals of Pure and Applied Logic, to appear.Google Scholar
[13]Pohlers, W., Proof theory: An introduction, Lecture Notes in Mathematics, vol. 1407, Springer, Berlin, 1989.CrossRefGoogle Scholar
[14]Rathjen, M., Proof-theoretic analysis of KPM, Archive for Mathematical Logic, vol. 30 (1991), pp. 377–403.CrossRefGoogle Scholar
[15]Rathjen, M., Collapsing functions based on recursively large ordinals: A wellordering proof for KPM, Archive for Mathematical Logic, vol. 33 (1994).CrossRefGoogle Scholar
[16]Schütte, K., Kennzeichnung von Ordnungszahlen durch rekursiv erklärte Funktionen, Mathematische Annalen, vol. 127 (1954), pp. 15–32.CrossRefGoogle Scholar
[17]Schütte, K., Proof theory, Springer, Berlin, 1977.CrossRefGoogle Scholar
[18]Setzer, A., Extending Martin-Löf type theory by one Mahlo universe, Archive for Mathematical Logic, vol. 39 (2000), pp. 155–181.CrossRefGoogle Scholar
[19]Strahm, T., Wellordering proofs for metapredicative Mahlo, this Journal, to appear.Google Scholar
[20]Strahm, T., First steps into metapredicativity in explicit mathematics, Sets and proofs (Cooper, S. B. and Truss, J., editors). Cambridge University Press, 1999, pp. 383–402.CrossRefGoogle Scholar
[21]Strahm, T., Autonomous fixed point progressions and fixed point transfinite recursion, Logic colloquium '98 (Buss, S., Hájek, P., and Pudlák, P., editors), vol. 13, ASL Lecture Notes in Logic, 2000, pp. 449–464.Google Scholar
[22]Troelstra, A. and van Dalen, D, Constructivism in mathematics, vol. I. North-Holland, Amsterdam, 1988.Google Scholar