caa a22 4500 388039159 CHVBK 20180307125016.0 cr unu---uuuuu 161130e199806 xx s 000 0 eng 10.2307/2586846 doi S0022481200015048 pii (NATIONALLICENCE)cambridge-10.2307/2586846 Rathjen Michael Department of Pure Mathematics, University of Leeds, England, E-mail: rathjen@amsta.leeds.ac.uk Explicit mathematics with the monotone fixed point principle [Elektronische Daten] [Michael Rathjen] 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. Copyright © Association for Symbolic Logic 1998 The Journal of Symbolic Logic Cambridge University Press 63/2(1998-06), 509-542 0022-4812 63:2<509 1998 63 JSL https://doi.org/10.2307/2586846 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.2307/2586846 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Rathjen Michael Department of Pure Mathematics, University of Leeds, England, E-mail: rathjen@amsta.leeds.ac.uk NATIONALLICENCE 773 0- The Journal of Symbolic Logic Cambridge University Press 63/2(1998-06), 509-542 0022-4812 63:2<509 1998 63 JSL CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence SWISSBIB 388039159 BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-cambridge