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

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).

## 1 Answer

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$$.

• Thanks! Can I also prove that every axiom of Intuitionistic Zermelo-Fraenkel set theory can be proved in Zermelo-Fraenkel set theory? Axioms 1,2,3,4,5,6 and 8 are all axioms of ZF. What about axioms 7 and 9? Commented Oct 13, 2022 at 10:32
• @effezeta We already covered 9 in my above answer since 9 is part of CZF. Note that 7 follows trivially from 7'' - in the presence of full separation, 7'' follows from 7. In fact, all axioms of CZF are theorems of IZF (formulated with 7), and all axioms of IZF are theorems of ZF. Commented Oct 13, 2022 at 16:24