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!

  • 5
    $\begingroup$ This is exactly the sort of thing the recursion theorem is for. $\endgroup$ Feb 16, 2013 at 15:49
  • $\begingroup$ Note that if you have the function $f:\omega\to\ \omega+\omega$, you already have $\mathrm{Cod}(f)=\omega+\omega$. And by removing all the finite sets from $\omega+\omega$ you are left with $\{\omega,\omega+1,...\}$ because that is how (von Neumann) ordinals work. No replacement needed. $\endgroup$
    – M. Winter
    May 19, 2017 at 8:17
  • $\begingroup$ @M.Winter I don't think we can define $f$ without using replacement. And how do we define $\omega + \omega$ as the codomain of $f$ without assuming that $\omega + \omega$ exists? $\endgroup$ Apr 27, 2022 at 19:42

1 Answer 1


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

  • $\begingroup$ 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? $\endgroup$
    – Jing Zhang
    Feb 16, 2013 at 16:10
  • $\begingroup$ @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. $\endgroup$ Feb 16, 2013 at 16:12
  • $\begingroup$ 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.\}$? $\endgroup$
    – Jing Zhang
    Feb 16, 2013 at 16:19
  • $\begingroup$ Oh I see. Thanks! $\endgroup$
    – Jing Zhang
    Feb 16, 2013 at 16:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .