The disjunction and related properties for constructive Zermelo-Fraenkel set theory

DOI10.2178/jsl/1129642124zbMath1100.03046OpenAlexW2056914778MaRDI QIDQ5486250

Michael Rathjen

Publication date: 6 September 2006

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1129642124

zbMATH Keywords

disjunction propertyconstructive Zermelo-Fraenkel set theoryregular extension axiomnumerical existence propertyChurch's rule

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items

CZF does not have the existence property ⋮ APPROXIMATING BEPPO LEVI’S PRINCIPIO DI APPROSSIMAZIONE ⋮ To be or not to be constructive, that is not the question ⋮ Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory ⋮ Choice and independence of premise rules in intuitionistic set theory ⋮ Numerical existence property and categories with an internal copy ⋮ Realisability for infinitary intuitionistic set theory ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ From the weak to the strong existence property ⋮ Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory ⋮ Kripke models for subtheories of \textsf{CZF} ⋮ Characterizing the interpretation of set theory in Martin-Löf type theory ⋮ Refinement is equivalent to Fullness ⋮ A categorical reading of the numerical existence property in constructive foundations ⋮ LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION

Cites Work

• Set existence property for intuitionistic theories with dependent choice
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Realizability and recursive set theory
• Constructivism in mathematics. An introduction. Volume I
• The strength of some Martin-Löf type theories
• Inaccessible set axioms may have little consistency strength
• The disjunction property implies the numerical existence property
• Formal systems for some branches of intuitionistic analysis
• A quasi-intumonistic set theory