Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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).

Thanks in advance!

share|cite|improve this question
This is exactly the sort of thing the recursion theorem is for. – Chris Eagle Feb 16 '13 at 15:49
up vote 4 down vote accepted

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$".

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.