Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-16T07:26:55.598Z Has data issue: false hasContentIssue false
  • English
  • Français

Explicit mathematics with the monotone fixed point principle

Published online by Cambridge University Press:  12 March 2014

Michael Rathjen
Michael Rathjen*
Affiliation:
Department of Pure Mathematics, University of Leeds, England, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The context for this paper is Feferman's theory of explicit mathematics, a formal framework serving many purposes. It is suitable for representing Bishop-style constructive mathematics as well as generalized recursion, including direct expression of structural concepts which admit self-application. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications (Feferman's notion of set) possesses a least fixed point. To be more precise, the new axiom not merely postulates the existence of a least solution, but, by adjoining a new functional constant to the language, it is ensured that a fixed point is uniformly presentable as a function of the monotone operation.

The upshot of the paper is that the latter extension of explicit mathematics (when based on classical logic) embodies considerable proof-theoretic strength. It is shown that it has at least the strength of the subsystem of second order arithmetic based on comprehension.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 63 , Issue 2 , June 1998 , pp. 509 - 542
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., An introduction to inductive definitions, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 739–782.10.1016/S0049-237X(08)71120-0Google Scholar
[2] Barwise, J. and Fischer, E., The Shoenfield absoluteness lemma, Israel Journal of Mathematics, vol. 8 (1970), pp. 329–339.10.1007/BF02798679Google Scholar
[3] Beeson, M., Foundations of constructive mathematics, Springer-Verlag, Berlin, 1985.10.1007/978-3-642-68952-9Google Scholar
[4] Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., Iterated inductive definitions and subsystems of analysis, Lecture Notes in Mathematics, no. 897, Springer-Verlag, Berlin, 1981.Google Scholar
[5] Cantini, A., On the relation between choice and comprehension principles in second order arithmetic, this Journal, vol. 51 (1986), pp. 360–373.Google Scholar
[6] Feferman, S., A language and axioms for explicit mathematics, Algebra and logic (Crossley, J. N., editor), Lecture Notes in Mathematics, no. 450, Springer-Verlag, Berlin, 1975, pp. 87–139.Google Scholar
[7] 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
[8] Feferman, S., Monotone inductive definitions, The L. E. J. Brouwer centenary symposium (Troelstra, A. S. and van Dalen, D., editors), North-Holland, Amsterdam, 1982, pp. 77–89.Google Scholar
[9] Feferman, S. and Sieg, W., Proof-theoretic equivalences between classical and constructive theories of analysis, Iterated inductive definitions and subsystems of analysis (Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., editors), Lecture Notes in Mathematics, no. 897, Springer-Verlag, Berlin, 1981, pp. 78–142.Google Scholar
[10] Friedman, H., Iterated inductive definitions and – AC, Intuitionism and proof theory (Kino, A., Myhill, J., and Vesley, R. E., editors), North-Holland, Amsterdam, 1968, pp. 435–442.Google Scholar
[11] Glass, T., Standardstrukturen für Systeme Expliziter Mathematik, Inaugural-Dissertation , Münster, 1993.Google Scholar
[12] Glass, T., Rathjen, M., and Schlüter, A., The strength of monotone inductive definitions in explicit mathematics, Annals of Pure and Applied Logic, vol. 85 (1997), pp. 1–46.Google Scholar
[13] Harrington, L. A., Kolmogorov's R-operator and the first nonprojectible ordinal, 13 pages, mimeographed notes, 1975.Google Scholar
[14] Hinman, P. G., Recursion-theoretic hierarchies, Springer, Berlin, 1978.Google Scholar
[15] John, T., Recursion in Kolmogorov's R-operator and the ordinal σ3 , this Journal, vol. 51 (1986), pp. 1–11.Google Scholar
[16] Kechris, A. S., Spector second order classes and reflection, Generalized recursion theory II (Fenstad, J. E., Gandy, R. O., and Sacks, G. E., editors), North-Holland, Amsterdam, 1978, pp. 147–183.Google Scholar
[17] Kechris, A. S. and Moschovakis, Y. N., Recursion in higher types, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 681–737.Google Scholar
[18] Moschovakis, Y. N., Elementary inductions on abstract structures, North–Holland, Amsterdam, 1974.Google Scholar
[19] Rathjen, M., Explicit mathematics with the monotone fixed point principle, II: Models, 33 pages, submitted.Google Scholar
[20] Rathjen, M., Monotone inductive definitions in explicit mathematics, this Journal, vol. 61 (1996), pp. 125–146.Google Scholar
[21] Richter, W. and Aczel, P., Inductive definitions and reflecting properties of admissible ordinals, Generalized recursion theory (Fenstad, J. E. and Hinman, P. G., editors), North-Holland, Amsterdam, 1974, pp. 301–381.Google Scholar
[22] Rogers, H., Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967.Google Scholar
[23] Schütte, K., Proof theory, Springer-Verlag, Berlin, 1977.10.1007/978-3-642-66473-1Google Scholar
[24] Schwichtenberg, H., Proof theory: Some applications of cut-elimination, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 867–895.10.1016/S0049-237X(08)71124-8Google Scholar
[25] Shoenfield, J. R., Mathematical logic, Addison-Wesley, 1967.Google Scholar
[26] Tait, W., Normal derivability in classical logic, The syntax and semantics of infinitary languages (Barwise, J., editor), Lectures Notes in Mathematics, no. 72, Springer-Verlag, Berlin, 1968, pp. 204–236.10.1007/BFb0079691Google Scholar
[27] Takahashi, S., Monotone inductive definitions in a constructive theory of functions and classes, Annals of Pure and Applied Logic, vol. 42 (1989), pp. 255–279.Google Scholar