Explicit mathematics with the monotone fixed point principle. II: Models
Journal of Symbolic Logic 64 (2):517-550 (1999)
| Abstract | This paper continues investigations of the monotone fixed point principle in the context of Feferman's explicit mathematics begun in [14]. 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. [14] 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. [14] 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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesGerhard 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).
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.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads1 ( #274,652 of 549,069 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
