CZF does not have the existence property

DOI10.1016/j.apal.2014.01.004zbMath1349.03086arXiv1303.3408OpenAlexW2013764776MaRDI QIDQ2637709

Andrew Swan

Publication date: 14 February 2014

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

Full work available at URL: https://arxiv.org/abs/1303.3408

zbMATH Keywords

realizabilityCZFexistence property

Mathematics Subject Classification ID

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

Related Items

Choice and independence of premise rules in intuitionistic set theory ⋮ Ordinal Analysis of Intuitionistic Power and Exponentiation Kripke Platek Set Theory ⋮ A cumulative hierarchy of sets for constructive set theory ⋮ A categorical reading of the numerical existence property in constructive foundations

Cites Work

• From the weak to the strong existence property
• Set existence property for intuitionistic theories with dependent choice
• On the constructive Dedekind reals
• Realizability. An introduction to its categorical side
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Realizability and recursive set theory
• Set theory. An introduction to independence proofs
• Constructivism in mathematics. An introduction. Volume II
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Church's thesis, continuity, and set theory
• Constructive set theory
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Formal systems for some branches of intuitionistic analysis
• On the interpretation of intuitionistic number theory
• The axiom of choice
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item