Metapredicative and explicit Mahlo: a proof-theoretic perspective

doi:10.1017/9781316755884.011

Metapredicative and explicit Mahlo: a proof-theoretic perspective

from ARTICLES

Published online by Cambridge University Press: 27 June 2017

Gerhard Jäger

Edited by

René Cori ,

Alexander Razborov ,

Stevo Todorčević and

Carol Wood

Show author details

René Cori: Affiliation:
Université de Paris VII (Denis Diderot)
Alexander Razborov: Affiliation:
Institute for Advanced Study, Princeton, New Jersey
Stevo Todorčević: Affiliation:
Université de Paris VII (Denis Diderot)
Carol Wood: Affiliation:
Wesleyan University, Connecticut

Book contents

Get access

Summary

Abstract. After briefly discussing the concepts of predicativity, metapredicativity and impredicativity, we turn to the notion of Mahloness as it is treated in various contexts. Afterwards the appropriate Mahlo axioms for the framework of explicit mathematics are presented. The article concludes with relating explicit Mahlo to certain nonmonotone inductive definitions.

Introduction. More than 100 years ago Cantor developed the theory of infinite sets (Cantor's paradise). Shortly afterwards,Russell found his famous paradox, and, as a consequence,manymathematicians became very concerned about the foundations of mathematics, and the expression foundational crisis was coined.

To overcome this crisis, Hilbert proposed the program of Beweistheorie as a method of rescuing Cantor's paradise. A few years later, however, Gödel showed that Hilbert's program—at least in its original strong form—cannot work. Again, after only a short while a first new idea was brought in by Gentzen, and a break-through along these lines was obtained by his prooftheoretic analysis of first order arithmetic. Then, during the last decades, Gentzen's work has been extended to stronger and stronger subsystems of second order arithmetic and set theory, most prominently by the schools of Schütte and Takeuti, leading to what today is denoted as infinitary and finitary proof theory, respectively.

A position completely different from Hilbert's was taken by Brouwer who advocated the restriction of mathematics to those principles which could be justified on constructive grounds. Starting off from his pioneering work various “dialects” of constructive mathematics have been put forward (e.g., in the Netherlands directly following Brouwer and Heyting, the Russian form(s) of constructivism, Bishop's approach, Martin-Löf type theory, Feferman's explicit mathematics).

In a certain sense the research directions originating from Hilbert's and Brouwer's original ideas come together again under the heading of reductive proof theory which tries to justify classical theories and classical principles by reducing them to a (more) constructive framework. For further reading and detailed information about this topic we refer, for example, to Beeson [6], Feferman [17] and Troelstra and van Dalen [61].

Type: Chapter
Information: Logic Colloquium 2000 , pp. 272 - 293

DOI: https://doi.org/10.1017/9781316755884.011 [Opens in a new window]

Publisher: Cambridge University Press

Print publication year: 2005

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

[1] Peter, Aczel, The type-theoretic interpretation of constructive set theory, Logic Colloquium '77 (A., MacIntyre,L., Pacholski, and J., Paris, editors), North-Holland, 1978, pp. 55–66.Google Scholar

[2] Peter, Aczel, The type-theoretic interpretation of constructive set theory: choice principles, The L.E.J.Brouwer Centenary Symposium (A.S., Troelstra and D., van Dalen, editors), North- Holland, 1982, pp. 1–40.

[3] Peter, Aczel, The type-theoretic interpretation of constructive set theory: inductive definitions, Logic, Methodology and Philosophy of Science VII (R.B., Marcus, G.J.W., Dorn, and P., Weingartner, editors), North-Holland, 1986, pp. 17–49.

[4] Peter, Aczel and Peter G., Hinman, Recursion in the superjump, Generalized Recursion Theory, Proceedings of the 1972 Symposium, Oslo (J.E., Fenstad and P.G., Hinman, editors), vol. 94, North-Holland, 1974, pp. 3–41.

[5] Jeremy, Avigad, On the relationship between ATR 0 and Id, The Journal of Symbolic Logic, vol. 61 (1996), no. 3, pp. 768–779.Google Scholar

[6] Michael J., Beeson, Foundations of ConstructiveMathematics: Metamathematical Studies, Springer, 1985.

[7] Laura, Crosilla, RealizabilityModels for Constructive Set Theories with Restricted Induction, Ph.D.|thesis, School of Mathematics, University of Leeds, 2000.

[8] Solomon, Feferman, Systems of predicative analysis, The Journal of Symbolic Logic, vol. 29 (1964), no. 1, pp. 1–30.Google Scholar

[9] Solomon, Feferman, A language and axioms for explicit mathematics,Algebra and Logic (J.N., Crossley, editor), Lecture Notes in Mathematics, vol. 450, Springer, 1975, pp. 87–139.

[10] Solomon, Feferman, Recursion theory and set theory: a marriage of convenience,Generalized Recursion Theory II, Oslo 1977 (J.E., Fenstad, R.O., Gandy, and G.E., Sacks, editors), North-Holland, 1978, pp. 55–98.

[11] Solomon, Feferman, Constructive theories of functions and classes, Logic Colloquium '78 (M., Boffa, D., van Dalen, and K., McAloon, editors), North-Holland, 1979, pp. 159–224.

[12] Solomon, Feferman, Iterated inductive fixed-point theories: application to Hancock's conjecture,The Patras Symposion (G., Metakides, editor), North-Holland, 1982, pp. 171–196.

[13] Solomon, Feferman,Weyl vindicated: “Das Kontinuum” 70 years later,Temi e Prospettive della Logica e della Filosofia della Scienza Contemporanee (C., Celluci and G., Sambin, editors), CLUEB, 1988, pp. 59–93.

[14] Solomon, Feferman, Polymorphic typed lambda-calculi in a type-free axiomatic framework,Logic and Computation (W., Sieg, editor), Contemporary Mathematics, vol. 106, American Mathematical Society, 1990, pp. 101–136.

[15] Solomon, Feferman, Logics for termination and correctness of functional programs,Logic from Computer Science (Y.N., Moschovakis, editor), Springer, 1991, pp. 95–127.

[16] Solomon, Feferman, Logics for termination and correctness of functional programs II: Logics of strength PRA,Proof Theory (P., Aczel, H., Simmons, and S.S., Wainer, editors), Cambridge University Press, 1992, pp. 195–225.

[17] Solomon, Feferman, Does reductive proof theory have a viable rationale?,Erkenntnis, vol. 53 (2000), pp. 63–96.Google Scholar

[18] Solomon, Feferman and Gerhard, Jäger, Systems of explicit mathematics with nonconstructive μ-operator. Part I,Annals of Pure and Applied Logic, vol. 65 (1993), no. 3, pp. 243–263.Google Scholar

[19] Solomon, Feferman and Gerhard, Jäger, Systems of explicit mathematics with non-constructive μ-operator. Part II,Annals of Pure and Applied Logic, vol. 79 (1996), no. 1, pp. 37–52.Google Scholar

[20] Harvey, Friedman, Some systems of second order arithmetic and their use,Proceedings of the International Congress of Mathematicians, Vancouver 1974, vol. 1, Canadian Mathematical Congress, 1975, pp. 235–242.

[21] Robin O., Gandy, General recursive functionals of finite type and hierarchies of functions,Annales de la Faculté des Sciences de l'Université de Clermont Ferrant, vol. 35 (1967), pp. 5–24.Google Scholar

[22] Leo, Harrington, The superjump and the first recursively Mahlo ordinal,Generalized Recursion Theory, Proceedings of the 1972 Symposium, Oslo (J.E., Fenstad and P.G., Hinman, editors), vol. 94, North-Holland, 1974, pp. 3–41.

[23] Gerhard, Jäger, Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Analysis,Ph.D.thesis, Universität München, 1979.

[24] Gerhard, Jäger, Theories for iterated jumps,Technical notes, Mathematical Institute, Oxford University, 1980.

[25] Gerhard, Jäger, Iterating admissibility in proof theory,Logic Colloquium '81. Proceedings of the Herbrand Symposion, North-Holland, 1982, pp. 137–146.

[26] Gerhard, Jäger, A well-ordering proof for Feferman's theory T0, Archiv für mathematische Logik und Grundlagenforschung, vol. 23 (1983), pp. 65–77.Google Scholar

[27] Gerhard, Jäger, The strength of admissibility without foundation,The Journal of Symbolic Logic, vol. 49 (1984), no. 3, pp. 867–879.Google Scholar

[28] Gerhard, Jäger, Induction in the elementary theory of types and names,Computer Science Logic '87 (E., Börger,H., Kleine Büning, and M.M., Richter, editors), Lecture Notes in Computer Science, vol. 329, Springer, 1988, pp. 118–128.

[29] Gerhard, Jäger, Type theory and explicit mathematics,Logic Colloquium '87 (H.-D., Ebbinghaus, J., Fernandez-Prida, M., Garrido,M., Lascar, and M., RodriguezArtalejo, editors), North-Holland, 1989, pp. 117–135.

[30] Gerhard, Jäger, The next admissible in set theories without foundation,Technical notes, Institut f ür Informatik und angewandteMathematik, Universität Bern, 1995.

[31] Gerhard, Jäger, First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo,The Journal of Symbolic Logic, vol. 66 (2001), pp. 1073–1089.CrossRef Google Scholar

[32] Gerhard, Jäger, Reinhard, Kahle, Anton, Setzer, and Thomas, Strahm, The prooftheoretic analysis of transfinitely iterated fixed point theories,The Journal of Symbolic Logic, vol. 64 (1999), no. 1, pp. 53–67.Google Scholar

[33] Gerhard, Jäger, Reinhard, Kahle, and Thomas, Studer, Universes in explicit mathematics,Annals of Pure and Applied Logic, vol. 109 (2001), pp. 141–162.Google Scholar

[34] Gerhard, Jäger and Wolfram, Pohlers, Eine beweistheoretische Untersuchung von (Δ12 -CA) + (BI) und verwandter Systeme,Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftlicheKlasse, 1982, pp. 1–28.

[35] Gerhard, Jäger and Thomas, Strahm, Fixed point theories and dependent choice,Archive for Mathematical Logic, vol. 39 (2000), no. 7, pp. 493–508.Google Scholar

[36] Gerhard, Jäger and Thomas, Strahm, Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory,The Journal of Symbolic Logic, vol. 66 (2001), pp. 935–958.Google Scholar

[37] Gerhard, Jäger and Thomas, Strahm, The proof-theoretic strength of the Suslin operator in applicative theories,Reflections on the foundations of mathematics (W., Sieg, R., Sommer, and C., Talcott, editors), Lecture Notes in Logic, vol. 15, A K Peters, 2002, pp. 270–292.

[38] Gerhard, Jäger and Thomas, Studer, Extending the system T0 of explicit mathematics: the limit and Mahlo axioms,Annals of Pure and Applied Logic, vol. 114 (2002), pp. 79–101.CrossRef Google Scholar

[39] Reinhard, Kahle, Uniform limit in explicit mathematics with universes,Technical report, IAM-97-002, Institut f ür Informatik und angewandteMathematik, Universität Bern, 1997.

[40] Paul, Mahlo, Über lineare transfinite Mengen,Berichte uber die Verhandlungen der königlich sächsischenGesellschaft derWissenschaften zu Leipzig,Mathematisch-PhysischeKlasse, vol. 63, 1911, pp. 187–225.Google Scholar

[41] Markus, Marzetta, Predicative Theories of Types and Names, Ph.D.thesis, Institut f ür Informatik und angewandteMathematik, Universität Bern, 1993.

[42] John, Myhill, Constructive set theory,The Journal of Symbolic Logic, vol. 40 (1975), no. 3, pp. 347–382.Google Scholar

[43] Michael, Rathjen, Proof-theoretic analysis of KPM, Archive for Mathematical Logic, vol. 30 (1991), pp. 377–403.Google Scholar

[44] Michael, Rathjen, The recursively Mahlo property in second order arithmetic,Mathematical Logic Quaterly, vol. 42 (1996), pp. 59–66.Google Scholar

[45] Michael, Rathjen, The higher infinite in proof theory,Logic Colloquium '95 (J., Makowsky and E., Ravve, editors), Lecture Notes in Logic, vol. 11, Springer, 1998, pp. 275–304.

[46] Michael, Rathjen, The superjump inMartin-Löf type theory,Logic Colloquium '98 (S., Buss, P., Hájek, and P., Pudlák, editors), Lecture Notes in Logic, vol. 13, Association for Symbolic Logic, 2000, pp. 363–386.

[47] W., Richter, Recursively Mahlo ordinals and inductive definitions,Logic Colloquium '69 (R.O., Gandy and C.E.M., Yates, editors), North-Holland, 1971, pp. 273–288.

[48] Christian, Rüede, Metapredicative Subsystems of Analysis,Ph.D.thesis, Institut f ür Informatik und angewandteMathematik, Univeristät Bern, 2000.

[49] Christian, Rüede, Transfinite dependent choice and model reflection,The Journal of Symbolic Logic, vol. 67 (2002), no. 3, pp. 1153–1168.Google Scholar

[50] Christian, Rüede, The proof-theoretic analysis of Σ11 transfinite dependent choice,Annals of Pure and Applied Logic, vol. 122 (2003), pp. 195–234.Google Scholar

[51] Kurt, Schütte, Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik,Archiv für Mathematische Logik und Grundlagen der Mathematik, vol. 7 (1964), pp. 45–60.Google Scholar

[52] Anton, Setzer, Extending Martin-Löf type theory by one Mahlo universe,Archive for Mathematical Logic, vol. 39 (2000), no. 3, pp. 155–181.Google Scholar

[53] Stephen G., Simpson, Set-theoretic aspects of ATR0, Logic Colloquium '80 (D., van Dalen,D., Lascar, and J., Smiley, editors), North-Holland, Amsterdam, 1982, pp. 255–271.

[54] Stephen G., Simpson, Σ11 and Π11 transfinite induction, Logic Colloquium '80 (D., van Dalen,D., Lascar, and J., Smiley, editors), North-Holland, Amsterdam, 1982, pp. 239–253.

[55] Thomas, Strahm, First steps into metapredicativity in explicit mathematics,Sets and Proofs (S., Barry Cooper and John, Truss, editors), Cambridge University Press, 1999, pp. 383–402.

[56] Thomas, Strahm, Autonomous fixed point progressions and fixed point transfinite recursion,Logic Colloquium '98 (S., Buss,P., Hájek, and P., Pudlák, editors), Lecture Notes in Logic, vol. 13, Association for Symbolic Logic, 2000, pp. 449–464.Google Scholar

[57] Thomas, Strahm, Wellordering proofs for metapredicative Mahlo,The Journal of Symbolic Logic, vol. 67 (2002), pp. 260–278.Google Scholar

[58] Thomas, Studer, Explicit mathematics: W-type, models,Master's thesis, Institut f ür Informatik und angewandteMathematik, 1997.Google Scholar

[59] Thomas, Studer,Constructive foundations for featherweight java,Proof Theory inComputer Science (R., Kahle,P., Schroeder-Heister, and R., Stärk, editors), Lecture Notes in Computer Science, vol. 2183, Springer, 2001, pp. 202–238.

[60] Thomas, Studer, A semantics for ﹛﹜ str : a calculus with overloading and late-binding,Journal of Logic and Computation, vol. 11 (2001), pp. 527–544.Google Scholar

[61] Anne S., Troelstra and D., van Dalen, Constructivism in Mathematics, vol. I and II, North-Holland, 1988.

[62] Sergei, Tupailo, Realization of analysis into explicit mathematics,The Journal of Symbolic Logic, vol. 66 (2001), pp. 1848–1864.Google Scholar

[63] Sergei, Tupailo, Realization of constructive mathematics into explicit mathematics: a lower bound for an impredicative Mahlo universe,Annals of Pure and Applied Logic, vol. 120 (2003), pp. 165–196.Google Scholar

Book contents

Metapredicative and explicit Mahlo: a proof-theoretic perspective

Summary

Access options

References

Save book to Kindle

Save book to Dropbox

Save book to Google Drive