The disjunction and related properties for constructive Zermelo-Fraenkel set theory
From MaRDI portal
Publication:5486250
DOI10.2178/jsl/1129642124zbMath1100.03046OpenAlexW2056914778MaRDI QIDQ5486250
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
disjunction propertyconstructive Zermelo-Fraenkel set theoryregular extension axiomnumerical existence propertyChurch's rule
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