David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 64 (2):517-550 (1999)
This paper continues investigations of the monotone fixed point principle in the context of Feferman's explicit mathematics begun in . Explicit mathematics is a versatile formal framework for representing Bishop-style constructive mathematics and generalized recursion theory. 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 constant to the language, it is ensured that a fixed point is uniformly presentable as a function of the monotone operation. Let T 0 + UMID denote this extension of explicit mathematics.  gave lower bounds for the strength of two subtheories of T 0 + UMID in relating them to fragments of second order arithmetic based on Π 1 2 comprehension.  showed that T $_0 \upharpoonright$ + UMID and T $_0 \upharpoonright$ + IND N + UMID have at least the strength of (Π 1 2 - CA) $\upharpoonright$ and (Π 1 2 - CA), respectively. Here we are concerned with the exact reversals. Let UMID N be the monotone fixed-point principle for subclassifications of the natural numbers. Among other results, it is shown that T $_0 \upharpoonright$ + UMID N and T $_0 \upharpoonright$ + IND N + UMID N have the same strength as (Π 1 2 - CA) $\upharpoonright$ and (Π 1 2 - CA), respectively. The results are achieved by constructing set-theoretic models for the aforementioned systems of explicit mathematics in certain extensions of Kripke-Platek set theory and subsequently relating these set theories to subsystems of second arithmetic
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Michael Rathjen (2005). The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory. Synthese 147 (1):81 - 120.
Michael Rathjen (2005). An Ordinal Analysis of Stability. Archive for Mathematical Logic 44 (1):1-62.
Gerhard Jäger (2013). Operational Closure and Stability. Annals of Pure and Applied Logic 164 (7-8):813-821.
Similar books and articles
Gerhard Jäger & Thomas Strahm (2001). Upper Bounds for Metapredicative Mahlo in Explicit Mathematics and Admissible Set Theory. Journal of Symbolic Logic 66 (2):935-958.
Sergei Tupailo (2001). Realization of Analysis Into Explicit Mathematics. Journal of Symbolic Logic 66 (4):1848-1864.
Gerhard Jäger (1997). Power Types in Explicit Mathematics? Journal of Symbolic Logic 62 (4):1142-1146.
Johan Van Benthem (2005). Minimal Predicates. Fixed-Points, and Definability. Journal of Symbolic Logic 70 (3):696 - 712.
Ralph Matthes (2002). Tarski's Fixed-Point Theorem and Lambda Calculi with Monotone Inductive Types. Synthese 133 (1-2):107 - 129.
Philip Kremer (2008). Supervaluation Fixed-Point Logics of Truth. Journal of Philosophical Logic 37 (5):407 - 440.
Thomas Glass (1996). On Power Set in Explicit Mathematics. Journal of Symbolic Logic 61 (2):468-489.
Sergei Tupailo (2004). On the Intuitionistic Strength of Monotone Inductive Definitions. Journal of Symbolic Logic 69 (3):790-798.
Michael Rathjen (1996). Monotone Inductive Definitions in Explicit Mathematics. Journal of Symbolic Logic 61 (1):125-146.
Michael Rathjen (1998). Explicit Mathematics with the Monotone Fixed Point Principle. Journal of Symbolic Logic 63 (2):509-542.
Added to index2009-01-28
Total downloads5 ( #255,802 of 1,410,043 )
Recent downloads (6 months)1 ( #177,059 of 1,410,043 )
How can I increase my downloads?