# Definability and the Separation and Replacement Axiom Schemata

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?

• Discussion of deriving the axiom scheme of separation needs the context of all the other axioms imposed, not just mention of the axiom scheme of replacement. Is it a textbook's formulation of the axioms of set theory you have in mind? If possible state them all here. Sep 15 '14 at 20:42
• I'm still in the market for a textbook, as it were. But I've added my understanding to some wikipedia sourced axioms, and included the axiom of the null set to make up for removing separation. Of course, I am ultimately interested in understanding how all of the axioms (and the consequences of changing them) interrelate in this context. Sep 15 '14 at 21:15
• Maybe it should be pointed out that "definability" is of elements and subsets of the universe. You're talking about provability, since we are interested in how one schema can be proved from another. Both objects are syntactic, whereas definability is a semantic notion. Sep 16 '14 at 9:04
• I read: "axiom schema of replacement ... asserts that the image of any set under any definable mapping is also a set." It seemed to me that the sets which exist solely due to separation might make new definable mappings. Sep 16 '14 at 18:40

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.

• Ah. Yes I see. I don't see why there also couldn't be "some" consequence, but I understand we can certainly pick a consequence that is (would have been) a separation axiom and get the contradiction. The direct proof is certainly more elegant, but this is the proof that helped me understand the situation. Thanks! Sep 16 '14 at 18:34

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.

• Supposing I want to form $\{ z \in X | \varphi(z, \vec{w}, X) \}$, without using Separation -- how do I know that $\varphi$ is still a valid formula without Separation? Or how do I know that the truth of $\varphi(z, \vec{w}, X)$ is the same after the Separation axioms are removed? Sep 15 '14 at 22:26
• @Jonny: What do you mean by "still a valid formula without Separation"? Whether a formula is well-formed or not does not depend on which axioms you have. Sep 16 '14 at 0:47
• Similarly, if you're doing model theory, once you're in a particular model, the truth of formulas doesn't depend on which axioms you have. The proof sketch in my answer shows exactly that if you have a model that satisfies Null Set and (every instance of) Replacement, this model will necessarily also satisfy (every instance of) Separation. Sep 16 '14 at 0:49
• Example: Separation asserts a set with certain properties exist in every model. Lets call it $a$. There exists $\omega$ many wff that can talk about $a$. Remove Separation. Are these wff 'valid'? (This might be silly, which is why I include the second question simply about the truth of $\varphi$) Sep 16 '14 at 0:52
• @Jonny: What do you mean by a wff being "valid"? (This word has a technical meaning in logic, but it doesn't seem to be what you're talking about). The meaning of a formula doesn't depend on any axioms -- it just depends on which sets exist in the model, independently of which axioms you're thinking of. Sep 16 '14 at 0:55