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||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Per Lindström (2006). Note on Some Fixed Point Constructions in Provability Logic. Journal of Philosophical Logic 35 (3):225 - 230.
Michael Rathjen (1996). Monotone Inductive Definitions in Explicit Mathematics. Journal of Symbolic Logic 61 (1):125-146.
Sergei Tupailo (2004). On the Intuitionistic Strength of Monotone Inductive Definitions. Journal of Symbolic Logic 69 (3):790-798.
Thomas Glass (1996). On Power Set in Explicit Mathematics. Journal of Symbolic Logic 61 (2):468-489.
Philip Kremer (2008). Supervaluation Fixed-Point Logics of Truth. Journal of Philosophical Logic 37 (5):407 - 440.
Ralph Matthes (2002). Tarski's Fixed-Point Theorem and Lambda Calculi with Monotone Inductive Types. Synthese 133 (1-2):107 - 129.
Johan Van Benthem (2005). Minimal Predicates. Fixed-Points, and Definability. Journal of Symbolic Logic 70 (3):696 - 712.
Gerhard Jäger (1997). Power Types in Explicit Mathematics? Journal of Symbolic Logic 62 (4):1142-1146.
Dieter Probst (2006). The Proof-Theoretic Analysis of Transfinitely Iterated Quasi Least Fixed Points. Journal of Symbolic Logic 71 (3):721 - 746.
Michael Rathjen (1999). Explicit Mathematics with the Monotone Fixed Point Principle. II: Models. Journal of Symbolic Logic 64 (2):517-550.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Recent downloads (6 months)0
How can I increase my downloads?