Constructive Zermelo-Fraenkel set theory is contained in Zermelo-Fraenkel set theory

Question

I'm searching for a book or an article that proves that if a statement can be proved in Constructive Zermelo-Fraenkel set theory then the statement can be proved in Zermelo-Fraenkel set theory (for example, I'm searching for a proof of the fact that every axiom of Constructive Zermelo-Fraenkel set theory can be proved in Zermelo-Fraenkel set theory).

Answer 1

Proving this is fairly straightforward. We follow this article’s definition.

Clearly, axioms 1, 2, 3, 4, 5, 6, 7’, and 8 are all axioms of ZF. We need to prove axiom 6’, 7’’, 8, and 9.

For 6’, note that every instance of 6’ is an instance of 6. So every axiom in 6’ (bounded separation) is already an axiom of ZF, since it is an instance of the axiom scheme of separation.

For 7’’ (strong collection), we use Scott’s Trick. Suppose $\forall x \in A \exists y \phi(x, y)$. Then for each $x \in A$, let $\alpha_x$ be the least ordinal such that $\exists y \in V_{\alpha_x} \phi(x, y)$. Then take $C = \bigcup\limits_{x \in A} V_{\alpha_x}$. And take $B = \{y \in C \mid \exists x \in A \phi(x, y)\}$. This is the $B$ that axiom 7’’ asserts.

For 8’, we take the form asserted in the article, $\forall A \forall B \exists C (C$ is full from $A$ to $B)$. This follows directly from the existence of power sets: let $C = \{R \in P(A \times B) \mid R$ is total$\}$.

For 9, suppose $\forall y (\forall a \in y \phi(a) \to \phi(y))$. Now suppose for sake of contradiction that there is some $x$ such that $\neg \phi(x)$. Let $T$ be the transitive closure of $\{x\}$, and let $U = \{u \in T \mid \neg \phi(u)\}$. By the axiom of regularity, take a $\in$-minimal element $w$ of $U$. Then for all $a \in w$, $a \notin U$ and thus $\phi(a)$. Therefore, $\phi(w)$. This contradicts $u \in U$.