CZF does not have the Existence Property

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.