CZF does not have the existence property
From MaRDI portal
Publication:2637709
Abstract: Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever (exists x)phi(x) is provable, there is a formula chi(x) such that (exists ! x)phi(x) wedge chi(x) is provable. It has been known since the 80's that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has remained open until now whether EP holds for the most well known constructive set theory, CZF. In this paper we show that EP fails for CZF.
Recommendations
- \(C_ 1\) is not algebraizable
- scientific article; zbMATH DE number 4208853
- scientific article; zbMATH DE number 3974957
- Non-existence of isomorphisms between certain unitals
- scientific article; zbMATH DE number 1889713
- Not every co-existential map is confluent
- scientific article; zbMATH DE number 978244
- An Étale realization which does NOT exist
- Consistently there is no non trivial ccc forcing notion with the Sacks or Laver property
- UHF algebras have neither property (FS') nor exponential rank 1
Cites work
- Characterizing the interpretation of set theory in Martin-Löf type theory
- Church's thesis, continuity, and set theory
- Constructive set theory
- Constructivism in mathematics. An introduction. Volume II
- Formal systems for some branches of intuitionistic analysis
- From the weak to the strong existence property
- 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 3900744 (Why is no real title available?)
- scientific article; zbMATH DE number 3937166 (Why is no real title available?)
- scientific article; zbMATH DE number 3754682 (Why is no real title available?)
- Metamathematical properties of intuitionistic set theories with choice principles
- On the constructive Dedekind reals
- On the interpretation of intuitionistic number theory
- Realizability and recursive set theory
- Realizability for constructive Zermelo-Fraenkel set theory
- Realizability. An introduction to its categorical side
- Set existence property for intuitionistic theories with dependent choice
- Set theory. An introduction to independence proofs
- The axiom of choice
- 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
- 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)- A categorical reading of the numerical existence property in constructive foundations
- Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
- From the weak to the strong existence property
- Metamathematical properties of intuitionistic set theories with choice principles
- A cumulative hierarchy of sets for constructive set theory
- The disjunction and related properties for constructive Zermelo-Fraenkel set theory
- Choice and independence of premise rules in intuitionistic set theory
- Very large set axioms over constructive set theories
- Set existence property for intuitionistic theories with dependent choice
This page was built for publication: CZF does not have the existence property
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2637709)
