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

DOI10.2178/JSL/1129642124zbMATH Open1100.03046OpenAlexW2056914778MaRDI QIDQ5486250FDOQ5486250

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

Recommendations

• Metamathematical properties of intuitionistic set theories with choice principles
• Realizability for constructive Zermelo-Fraenkel set theory
• CZF does not have the existence property
• Constructive set theory and Brouwerian principles
• Characterizing the interpretation of set theory in Martin-Löf type theory

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) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35)

Cites Work

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

Cited In (25)

• From the weak to the strong existence property
• Disjunctive systems and L-Domains
• Characterizing the interpretation of set theory in Martin-Löf type theory
• The logic of multisets continued: The case of disjunction
• Constructive set theory and Brouwerian principles
• Lifschitz realizability as a topological construction
• Realisability for infinitary intuitionistic set theory
• Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory
• Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
• To be or not to be constructive, that is not the question
• Derived rules for predicative set theory: an application of sheaves
• Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)
• Disjoint essential sets of implicates of a CQ Horn function
• Kripke models for subtheories of \textsf{CZF}
• Realizability for constructive Zermelo-Fraenkel set theory
• Metamathematical properties of intuitionistic set theories with choice principles
• Approximating Beppo Levi's \textit{principio di approssimazione}
• Refinement is equivalent to fullness
• A categorical reading of the numerical existence property in constructive foundations
• Numerical existence property and categories with an internal copy
• Eliminating disjunctions by disjunction elimination
• Choice and independence of premise rules in intuitionistic set theory
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• CZF does not have the existence property

This page was built for publication: The disjunction and related properties for constructive Zermelo-Fraenkel set theory

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