From the weak to the strong existence property

DOI10.1016/j.apal.2012.01.012zbMath1259.03076OpenAlexW2059656706WikidataQ59902306 ScholiaQ59902306MaRDI QIDQ448335

Michael Rathjen

Publication date: 6 September 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2012.01.012

zbMATH Keywords

realizabilityintuitionistic set theoryexistence propertyset recursive functionsweak existence property

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Related Items

CZF does not have the existence property, INDEFINITENESS IN SEMI-INTUITIONISTIC SET THEORIES: ON A CONJECTURE OF FEFERMAN, APPROXIMATING BEPPO LEVI’S PRINCIPIO DI APPROSSIMAZIONE, Relativized ordinal analysis: the case of power Kripke-Platek set theory, Constructing the constructible universe constructively, Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory, The scope of Feferman's semi-intuitionistic set theories and his second conjecture

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• Set existence property for intuitionistic theories with dependent choice
• Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Constructivism in mathematics. An introduction. Volume II
• Power set recursion
• Functional interpretation of Aczel's constructive set theory
• Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Lifschitz' realizability
• Disjunction and existence under implication in elementary intuitionistic formalisms
• Constructive set theory
• CT 0 is Stronger than CT 0 !
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• IKP and friends
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Formalized recursive functionals and formalized realizability
• Formal systems for some branches of intuitionistic analysis
• A quasi-intumonistic set theory
• On the interpretation of intuitionistic number theory