# Axiom of replacement

I want to prove the existence of $\{\omega, \omega+1,\cdots\}$ using axiom of replacement by defining a function $f:\omega \mapsto \omega+\omega$ with $f(n)=\omega+n$. But the class function needs to be definable by some formula. I am not very sure of how to write that formula explicitly. (Within ZFC).

-
This is exactly the sort of thing the recursion theorem is for. – Chris Eagle Feb 16 '13 at 15:49

This sort of thing is in general the function of the recursion theorem. Here's how it works in this specific case:

We have a recursively defined "function" $F$, which we want to show can actually be expressed by a formula (and hence, by replacement, by a bona fide function). $F$ needs to be defined on $\omega$ and to satisfy

1. $F(0)=\omega$
2. $F(s(n))=s(F(n))$

where $s$ is the successor function.

Say that a function $f$ is an attempt at defining $F$ if its domain is an initial segment of $\omega$, and it satisfies the above equations whenever they make sense. All this can be easily expressed as a formula:

$$(f \text{ is a function}) \land (\exists n \in \omega (\mathrm{dom}(f)=n))\land (0 \in \mathrm{dom}(f) \to f(0)=\omega) \land (\forall n \in \omega (s(n)\in \mathrm{dom}(f) \to f(s(n))=s(f(n))))$$

It's easy to prove by induction that for any $n$, there's an attempt defined at $n$, and that any two attempts agree on the intersections of their domains. We can thus define $F$ by declaring $F(a)=b$ to mean "there exists an attempt $f$ defined at $a$ with $f(a)=b$".

-
Thanks! But the problem is whether "there exists an attempt f defined at a with f(a)=b" is definable in some first-order formula? Say $f_n$ is the n-initial approximation, then $\exists n f_n \cdots$ is not really a formula, is it? – Jing Zhang Feb 16 '13 at 16:10
@Jing: What do "n-initial approximations" have to do with anything? I've explained what "attempt" means. Do you not see how to write "f is an attempt" as a formula? That should be tedious but not actually difficult. – Chris Eagle Feb 16 '13 at 16:12
I see how to write a finite function as formula. But I'm not sure how you use the approximations to define $F$ using some formula in the language $L=\{\in,\exists,\forall,(,),etc.\}$? – Jing Zhang Feb 16 '13 at 16:19
Oh I see. Thanks! – Jing Zhang Feb 16 '13 at 16:30