Definability and the Separation and Replacement Axiom Schemata

Question

I am beginning to study Set Theory, so naturally one might begin with the axioms. When reading the schemata of separation and replacement, my initial thought was, "Why would we need separation if we have replacement? It seems like the sets which exist as a consequence of the separation axioms would also exist as a consequence of replacement." Sure enough, there is a question here on stack exchange asking exactly this. The answer seems to indicate yes, there is a proof indicating that replacement implies separation. Perhaps this is the case, but I'm not buying it yet.

I have a notion in my head that the set of definable functions available to the schema of replacement would be severely limited without already having the separation axioms. Perhaps the definable functions would be so limited that there might exist a set that exists due to separation that would be impossible to show exist due to the replacement axioms without separation. Or perhaps the two build on each other, in a sense that each set that exists due to a separation axiom spawns a set of new replacement axioms, each of which in turn define more sets that spawn more separation axioms, etc etc etc.

I believe working toward a proof of this kind may be very helpful in my understanding of the axioms, but I am having trouble setting up my proof. How do I formally talk about the set of definable functions available to a set theory axiom? There seems to be some weird self-reference going on here.

I would like to work in pure set-theory language: only variable symbols, $\in$, and first order logic symbols. Of course anything like $=$ and $\subset$ that are definable from these are allowed.

---

The axioms:

1. Null set: $\exists X \forall y (y \notin x)$

2. Extensionality: $\forall X \forall Y ( \forall z (z \in X \iff z \in Y) \implies X = Y$

3. Regularity: $\forall X ( (\exists a : a \in X) \implies \exists b (b \in X \land \neg \exists c (c \in b \land c \in X)))$

4. Separation: $\forall \vec{w} \forall X \exists Y \forall z (z \in Y \iff (z \in X \land \varphi(z, \vec{w}, X ) )) $

5. Pairing: $\forall x \forall y \exists z (x \in z \land y \in z)$

6. Union: $\forall X \exists Y \forall a \forall b ( (b \in a \land a \in X) \implies (b \in Y) ) $

7. Replacement: $\forall \vec{w} \forall A ( (\forall x \in A \exists ! y \varphi(x,y,\vec{w}, A) \implies (\exists B \forall y (y \in B \iff \exists x \in A \varphi(x,y,\vec{w}, A))))$

8. Infinity: $ \exists X ( \emptyset \in X \land \forall y (y \in X \implies y \cup \{ y \} \in X))$

9. Power Set: $\forall x \exists y \forall z (z \subseteq x \implies z \in y) $

10. Choice, if it makes a difference here.

---

Further clarification:

If separation follows from replacement, then every model of ZF is a model of ZF without separation (ZF-S).

Assume separation does not follow from replacement. Then there exists a $\psi$ which is a consequence of ZF, but not a consequence of ZF-S. In fact there might be a $\psi$ that is false in every model of ZF-S. When $\psi$ has something to do with the $\varphi$ included in the axioms of replacement, the same axiom will assert the existence of a set with different properties in ZF than it would in ZF-S. Seems reasonable to me. Where could I find a contradiction?

Answer 1

Henning answered the original question fairly well. Let me address the clarification.

The proof that Replacement implies Separation can be really just put into reverse gear here. If Separation wasn't a consequence of $\sf ZF-S$, then you can find some formula $\varphi(x,p_1,\ldots,p_n)$ whose corresponding separation axiom is false in a model of $\sf ZF-S$.

It's not just "some" consequence. You can immediately say that this "consequence" is one of the separation axioms, and thus find some formula from which that axiom was defined.

Now just repeat the usual proof that Replacement implies Separation applied to that formula. And we will have that the statement we thought is consistently false with $\sf ZF-S$ is really provable from that theory. So it's a contradiction.

But of course, all that really just shows that you should prove this directly. Like the usual proof goes.

Answer 2

Suppose you want to form $\{z\in X\mid \varphi(z,\vec w,X)\}$, without using Separation.

Either there exists $z$ such that $z\in X\land \varphi(z,\vec w,X)$ or there doesn't. In the latter case, the set you're after is the empty set, whose existence is given by axiom 0.

Otherwise, let $Z$ be one such $z$, and then apply Replacement with $A'=X$, $\vec w'=\vec w\|Z$ and $$ \varphi'(x,y,\vec w,Z,X) \equiv (\varphi(x,\vec w,X) \land y=x) \lor (\neg\varphi(x,\vec w,X) \land y=Z) $$ (where primed variables are those that appear in Replacement, and the unprimed are the ones we already have). Then the $\exists!$ part of Replacement is trivial, and the $B$ you get is the desired subset of $X$.

---

There's nothing particularly circular here -- if you have a proof that involves both Separation and Replacement you can mechanically replace all instances of Separation using the above proof schema, and this gives you a proof of the original theorem that doesn't use Separation.