Axiom of replacement examples

Question

I've been trying to understand the axiom of replacement for quite a while now, I really don't get it, I don't understand how it can be used to show that a class is a set in ZF. My textbook gives me this definition:

I don't understand how this $\phi(s,t)$ formula has to be chosen and what it has to look like.

An example (that is not really an exmaple, since it's used in a proof) this book gives me is:

"Call $g$ an $n$-function, $g_n$, for $n∈ℕ$, if the following hold:

1. $g$ is a function
2. the domain of $g$ is the set $n^+$
3. $g(0)=y_0$
4. for all $i∈n$, $g$ satisfies the rule $g(i^+)=h(i,g(i))$

define $f$ to be: $f=⋃\{g_n:n∈ℕ\}$

We must show that this $f$ is a set in ZF. This follows from the union axiom once we have shown that $\{g_n:n∈ℕ\}$ is a set. And this latter follow from the axiom of replacement taking the formula $\phi(s,t)$ to be $(s∈ℕ→(t$ is an $s$-function$))∧(s∉ℕ→t=∅)$

We have shown that for each natural number $n$ there is a unique $n$-function so that $\phi(s,t)$ is a class function. Taking $x$ in the axiom of replacement to be the set $ℕ$, the resulting set of images is $\{g_n:n∈ℕ\}$, so that the latter is indeed a set."

But I still don't understand why that $\phi(s,t)$ is like that.

Can you guys give me an easier example for applying this theorem? for example, how can i prove that $\{1,2,3\}$ is a a set in ZF? How do i define this set $y$ such that $∃x'∈\{1,2,3\}∧\phi(x',y')$ where $\phi(x',y')$ is a class function?

Thank you!

Answer 1

There's no such thing as the axiom of replacement; it's the axiom schema of replacement. This means each binary predicate $\phi$ on sets contributes its own axiom to the schema. In particular, it would be more helpful to write the schema's special case with a given $\phi$ as$$\color{red}{(\forall s\exists t(\phi(s,\,t)\land\forall t^\prime(\phi(s,\,t^\prime)\to t^\prime=t)))}\to\color{blue}{(\forall x\exists y\forall y^\prime(y^\prime\in y\iff\exists x^\prime(x^\prime\in x\land\phi(x^\prime,\,y^\prime))))}.$$A typical proof strategy is to choose a $\phi$ for which you can prove the red part, so we then get the blue part from the relevant axiom within the schema. In fact, we can change the red part to$$\forall s\forall t\forall t^\prime(\phi(s,\,t)\land\phi(s,\,t^\prime)\to t^\prime=t),$$i.e. $\phi$ doesn't have to be satisfiable for all $s$.