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)|
References found in this work BETA
Monotone Inductive Definitions in a Constructive Theory of Functions and Classes.Shuzo Takahashi - 1989 - Annals of Pure and Applied Logic 42 (3):255-297.
On the Proof-Theoretic Strength of Monotone Induction in Explicit Mathematics.Thomas Glaß, Michael Rathjen & Andreas Schlüter - 1997 - Annals of Pure and Applied Logic 85 (1):1-46.
Citations of this work BETA
A New Model Construction by Making a Detour Via Intuitionistic Theories II: Interpretability Lower Bound of Feferman's Explicit Mathematics T 0.Kentaro Sato - 2015 - Annals of Pure and Applied Logic 166 (7-8):800-835.
Similar books and articles
Monotone Inductive Definitions in Explicit Mathematics.Michael Rathjen - 1996 - Journal of Symbolic Logic 61 (1):125-146.
On the Intuitionistic Strength of Monotone Inductive Definitions.Sergei Tupailo - 2004 - Journal of Symbolic Logic 69 (3):790-798.
On Power Set in Explicit Mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
Tarski's Fixed-Point Theorem and Lambda Calculi with Monotone Inductive Types.Ralph Matthes - 2002 - Synthese 133 (1-2):107 - 129.
Minimal Predicates. Fixed-Points, and Definability.Johan Van Benthem - 2005 - Journal of Symbolic Logic 70 (3):696 - 712.
Power Types in Explicit Mathematics?Gerhard Jäger - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
The Proof-Theoretic Analysis of Transfinitely Iterated Quasi Least Fixed Points.Dieter Probst - 2006 - Journal of Symbolic Logic 71 (3):721 - 746.
Explicit Mathematics with the Monotone Fixed Point Principle. II: Models.Michael Rathjen - 1999 - Journal of Symbolic Logic 64 (2):517-550.
Added to index2009-01-28
Total downloads163 ( #28,140 of 2,164,577 )
Recent downloads (6 months)1 ( #347,948 of 2,164,577 )
How can I increase my downloads?