How do the separation axioms follow from the replacement axioms?

It has come to my attention that the pairing axiom and the separation axiom schema are rarely listed since they follows from the replacement axioms. I see how this works for the pairing axiom, since we can take some set, say $A=\{\emptyset,\{\emptyset\}\}$, which exists by the power set axiom and the existence of the emptyset, and define a nominating formula on $A$ by $$ \phi(u,v)\colon (u=\emptyset\land v=a)\lor(u\neq\emptyset\land v=b) $$ to see that $\{a,b\}$ is a set for any sets $a$ and $b$. However, I don't see it for the separation schema. Could someone enlighten me on how they follow? Thanks.

Solution 1:

The replacement axiom (axiom scheme) is the most general form you need, essentially saying that if you have a function whose domain is a set then the image is also a set. Furthermore, the empty set can be inferred by an existence of any set at all, when combined with separation (and hence, can be inferred by replacement).

Formally speaking the replacement schema says that for every formula $\varphi(u,v,p_1,\ldots,p_n)$, fix the parameters $p_1,\ldots,p_n$ and pick any set $A$, whenever $u\in A$ has at most one $v$ for which $\varphi(u,v,p_1,\ldots,p_n)$ is true, then the collection of $\{v\mid\varphi(u,v,p_1,\ldots,p_n), u\in A\}$ is also a set.

How to infer separation and pairing? Simple.

First we infer separation. Given $\phi(x)$, we simply define $\varphi(u,v,p)$ to be $$\varphi(u,v,p)\stackrel{\text{def}}{=} u=v\land u\in p\land\phi(u)$$ This is a functional formula (i.e. for every $u$ there is at most a single $v$ for which $\varphi(u,v,p)$ holds) and it is easy to verify that the image of $\varphi(u,v,a)$ is indeed $\{x\in a\mid \phi(x)\}$.

The empty set exists by separation - simply take some $a$ (which exists because we assume there is some set in the universe) and the function $\phi(x)\colon = x\neq x$.

As you noted, $\{\emptyset ,P(\emptyset)\}$ exists by the Power set axiom.

Now for a given $x,y$ we want to have $\{x,y\}$ so we define the following $\varphi(u,v)$ as following: $$\varphi(u,v) \colon = (u=\emptyset\wedge v=x)\vee (u=P(\emptyset)\wedge v=y)$$

Note that $\varphi$ is a functional formula, i.e. for a given $u$ there is only one $v$ for which $\varphi(u,v)$ is true. By the axiom of replacement we have now that $\{x,y\}$ is a set. Therefore the axiom of pairing holds if we assume Power set and Replacement.

Now we have two ways of looking at ZFC. Sometimes we want to prove that something is a model for ZFC and need to verify the list of axioms in which case proving both Separation and Replacement is completely redundant. At other times we want to prove certain things which are quicker when using the more specific axioms (e.g. pairing (or even ordered pairing, which can be quickly inferred from pairing itself)).

This is a sort of freedom that we allow ourselves. We add extra axioms that we don't really need. Then if we want to ensure all the axioms hold we check for the "core" of the axiomatic system, and when we want to ease on ourselves in other cases we can just use the extra axioms for our convenience.

Solution 2:

Given a set $A$ and a formula $\phi(x)$ we create the function-class that sends every element $a\in A$ to $\{a\}$ if $\phi(a)$ and to $\varnothing$ otherwise. Typically this would be written $$\psi(x,y): (\phi(x)\to y=\{x\})\land(\lnot\phi(x)\to y=\varnothing)$$

Then taking the union of the set that is produced through the axiom of replacement you get what you are looking for.