Explicit mathematics with the monotone fixed point principle
Journal of Symbolic Logic 63 (2):509-542 (1998)
| 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 Π 1 2 comprehension | |||||||||
| 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,653 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesPer Lindström (2006). Note on Some Fixed Point Constructions in Provability Logic. Journal of Philosophical Logic 35 (3):225 - 230.
Dieter Probst (2006). The Proof-Theoretic Analysis of Transfinitely Iterated Quasi Least Fixed Points. Journal of Symbolic Logic 71 (3):721 - 746.
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 (1999). Explicit Mathematics with the Monotone Fixed Point Principle. II: Models. Journal of Symbolic Logic 64 (2):517-550.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads0Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
