From the weak to the strong existence property

DOI10.1016/J.APAL.2012.01.012MaRDI QIDQ448335zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Recommendations

• CZF does not have the existence property
• Set existence property for intuitionistic theories with dependent choice
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Some properties of epistemic set theory with collection
• scientific article; zbMATH DE number 3841848

Cites work

• scientific article; zbMATH DE number 432707 (Why is no real title available?)
• scientific article; zbMATH DE number 3427308 (Why is no real title available?)
• scientific article; zbMATH DE number 3427309 (Why is no real title available?)
• scientific article; zbMATH DE number 3425598 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3668598 (Why is no real title available?)
• scientific article; zbMATH DE number 3494394 (Why is no real title available?)
• scientific article; zbMATH DE number 1176133 (Why is no real title available?)
• scientific article; zbMATH DE number 5064954 (Why is no real title available?)
• scientific article; zbMATH DE number 3259043 (Why is no real title available?)
• scientific article; zbMATH DE number 3329865 (Why is no real title available?)
• A quasi-intumonistic set theory
• CT 0 is Stronger than CT 0 !
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Constructive set theory
• Constructivism in mathematics. An introduction. Volume II
• Disjunction and existence under implication in elementary intuitionistic formalisms
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Formal systems for some branches of intuitionistic analysis
• Formalized recursive functionals and formalized realizability
• Functional interpretation of Aczel's constructive set theory
• Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)
• IKP and friends
• Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory
• Lifschitz' realizability
• Metamathematical properties of intuitionistic set theories with choice principles
• On the interpretation of intuitionistic number theory
• Power set recursion
• Realizability for constructive Zermelo-Fraenkel set theory
• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• Set existence property for intuitionistic theories with dependent choice
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• The formulae-as-classes interpretation of constructive set theory
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories

Cited in

(9)

• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• CZF does not have the existence property
• Indefiniteness in semi-intuitionistic set theories: on a conjecture of Feferman
• Constructing the constructible universe constructively
• The scope of Feferman's semi-intuitionistic set theories and his second conjecture
• Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
• Set existence property for intuitionistic theories with dependent choice
• Some properties of epistemic set theory with collection
• Approximating Beppo Levi's \textit{principio di approssimazione}

This page was built for publication: From the weak to the strong existence property

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q448335)