CZF does not have the Existence Property
Andrew W Swan

TL;DR
This paper proves that the Constructive ZF (CZF) set theory does not possess the existence property, highlighting a significant metamathematical limitation of CZF compared to other constructive theories.
Contribution
It establishes for the first time that CZF fails the existence property, clarifying its limitations in constructive metamathematics.
Findings
EP fails for CZF
CZF lacks the set existence property
Implications for constructive set theory
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
