Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-12-01T09:11:19.687Z Has data issue: false hasContentIssue false
  • English
  • Français

Wellordering proofs for metapredicative Mahlo

Published online by Cambridge University Press:  12 March 2014

Thomas Strahm
Thomas Strahm*
Affiliation:
Universität Bern, Institut für Informatik und Angewandte Mathematik, Neubrückstrasse 10, CH-3012 Bern, Switzerland, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this article we provide wellordering proofs for metapredicative systems of explicit mathematics and admissible set theory featuring suitable axioms about the Mahloness of the underlying universe of discourse. In particular, it is shown that in the corresponding theories EMA of explicit mathematics and KPm0 of admissible set theory, transfinite induction along initial segments of the ordinal φω00, for φ being a ternary Veblen function, is derivable. This reveals that the upper bounds given for these two systems in the paper Jäger and Strahm [11] are indeed sharp.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 67 , Issue 1 , March 2002 , pp. 260 - 278
Copyright
Copyright © Association for Symbolic Logic 2002

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]Beeson, M. J., Foundations of Constructive Mathematics: Metamathematical Studies, Springer, Berlin, 1985.CrossRefGoogle Scholar
[2]Feferman, S., A language and axioms for explicit mathematics, Algebra and Logic (Crossley, J., editor), Lecture Notes in Mathematics, vol. 450, 1975, pp. 87–139.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, 1979, pp. 159–224.Google Scholar
[4]Feferman, S., Iterated inductive fixed-point theories: Application to Hancock's conjecture, The Patras Symposion (Metakides, G., editor), North Holland, 1982, pp. 171–196.CrossRefGoogle Scholar
[5]Feferman, S., Reflecting on incompleteness, this Journal, vol. 56 (1991), no. 1, pp. 1–49.Google Scholar
[6]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
[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, vol. 109 (2001), no. 3, pp. 141–162.CrossRefGoogle Scholar
[10]Jäger, G. and Strahm, T., Fixed point theories and dependent choice, Archive for Mathematical Logic, vol. 39 (2000), pp. 493–508.Google Scholar
[11]Jäger, G. and Strahm, T., Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory, this Journal, vol. 66 (2001), no. 2, pp. 935–958.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]Kahle, R., Applikative theorien und frege-strukturen, Ph.D. thesis, Institut für Informatik und angewandte Mathematik, Universität Bern, 1997.Google Scholar
[14]Marzetta, M., Predicative theories of types and names, Ph.D. thesis, Institut für Informatik und angewandte Mathematik, Universität Bern, 1993.Google Scholar
[15]Pohlers, W., Proof Theory: An introduction, Lecture Notes in Mathematics, vol. 1407, Springer, Berlin, 1989.CrossRefGoogle Scholar
[16]Rathjen, M., Proof-theoretic analysis of KPM, Archive for Mathematical Logic, vol. 30 (1991), pp. 377–403.CrossRefGoogle Scholar
[17]Rathjen, M., Collapsing functions based on recursively large ordinals: A wellordering proof for KPM, Archive for Mathematical Logic, vol. 33 (1994).CrossRefGoogle Scholar
[18]Rathjen, M., The strength of Martin-Löf type theory with a superuniverse. Part I, Archive for Mathematical Logic, vol. 39 (2000), no. 1, pp. 1–39.CrossRefGoogle Scholar
[19]Rathjen, M., The strength of Martin-Löf type theory with a superuniverse. Part II, Archive for Mathematical Logic, vol. 40 (2001), no. 3, pp. 207–233.CrossRefGoogle Scholar
[20]Rüede, C., Metapredicative subsystems of analysis, Submitted for publication.Google Scholar
[21]Rüede, C., The proof-theoretic analysis of Σ11 transfinite dependent choice, Submitted for publication.Google Scholar
[22]Rüede, C., Universes in metapredicative analysis. Submitted for publication.Google Scholar
[23]Rüede, C., Metapredicative subsystems of analysis, Ph.D. thesis, Institut für Informatik und angewandte Mathematik, Univeristät Bern, 2000.Google Scholar
[24]Schütte, K., Kennzeichnung von Ordnungszahlen durch rekursiv erklärte funktionen, Mathematische Anttaien, vol. 127 (1954), pp. 15–32.CrossRefGoogle Scholar
[25]Schütte, K., Proof Theory, Springer, Berlin, 1977.CrossRefGoogle Scholar
[26]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
[27]Strahm, T., Autonomous fixed point progressions and fixed point transfinite recursion, Logic Colloquium '98 (Buss, S., Hájek, P., and Pudlák, P., editors), Lecture Notes in Logic, vol. 13, Association for Symbolic Logic, 2000, pp. 449–464.Google Scholar
[28]Troelstra, A. and van Dalen, D., Constructivism in Mathematics, vol. I, North Holland, Amsterdam, 1988.Google Scholar