Switch to: References

Citations of:

On the proof-theoretic strength of monotone induction in explicit mathematics

Thomas Glaß, Michael Rathjen & Andreas Schlüter

Annals of Pure and Applied Logic 85 (1):1-46 (1997)

Add citations

You must login to add citations.

Intuitionistic fixed point logic.Ulrich Berger & Hideki Tsuiki - 2021 - Annals of Pure and Applied Logic 172 (3):102903.details We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how (...) Download Export citation Bookmark
On the intuitionistic strength of monotone inductive definitions.Sergei Tupailo - 2004 - Journal of Symbolic Logic 69 (3):790-798.details We prove here that the intuitionistic theory $T_{0}\upharpoonright + UMID_{N}$ , or even $EEJ\upharpoonright + UMID_{N}$ , of Explicit Mathematics has the strength of $\prod_{2}^{1} - CA_{0}$ . In Section I we give a double-negation translation for the classical second-order $\mu-calculus$ , which was shown in [ $M\ddot{o}02$ ] to have the strength of $\prod_{2}^{1}-CA_{0}$ . In Section 2 we interpret the intuitionistic $\mu-calculus$ in the theory $EETJ\upharpoonright + UMID_{N}$ . The question about the strength of monotone inductive definitions in (...) Download Export citation Bookmark 4 citations
Explicit mathematics with the monotone fixed point principle.Michael Rathjen - 1998 - Journal of Symbolic Logic 63 (2):509-542.details 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 (...) Download Export citation Bookmark 1 citation
Explicit mathematics with the monotone fixed point principle. II: Models.Michael Rathjen - 1999 - Journal of Symbolic Logic 64 (2):517-550.details 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 (...) Download Export citation Bookmark 6 citations
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.details Download Export citation Bookmark 5 citations
Explicit mathematics: power types and overloading.Thomas Studer - 2005 - Annals of Pure and Applied Logic 134 (2-3):284-302.details Systems of explicit mathematics provide an axiomatic framework for representing programs and proving properties of them. We introduce such a system with a new form of power types using a monotone power type generator. These power types allow us to model impredicative overloading. This is a very general form of type dependent computation which occurs in the study of object-oriented programming languages. We also present a set-theoretic interpretation for monotone power types. Thus establishing the consistency our system of explicit mathematics. Download Export citation Bookmark

1