David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 63 (2):509-542 (1998)
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)|
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
Shuzo Takahashi (1989). Monotone Inductive Definitions in a Constructive Theory of Functions and Classes. Annals of Pure and Applied Logic 42 (3):255-297.
Thomas Glaß, Michael Rathjen & Andreas Schlüter (1997). On the Proof-Theoretic Strength of Monotone Induction in Explicit Mathematics. Annals of Pure and Applied Logic 85 (1):1-46.
Citations of this work BETA
Kentaro Sato (2015). A New Model Construction by Making a Detour Via Intuitionistic Theories II: Interpretability Lower Bound of Feferman's Explicit Mathematics T 0. Annals of Pure and Applied Logic 166 (7-8):800-835.
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.
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):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 (1999). Explicit Mathematics with the Monotone Fixed Point Principle. II: Models. Journal of Symbolic Logic 64 (2):517-550.
Added to index2009-01-28
Total downloads162 ( #22,060 of 1,902,209 )
Recent downloads (6 months)58 ( #10,958 of 1,902,209 )
How can I increase my downloads?