# Definition of class function

In ZFC set theory, as usual let $\omega$ be the set of natural numbers and $V$ the universe, which is a proper class.

I want to define a "class function" $F : \omega \to V$ by $n \mapsto \omega + n$.

(Actually, the final aim is to show, using the axiom of replacement, that $$\{ \omega , \omega + 1 , \omega + 2 , \ldots \}= \{ \omega + n \, | \, n \in \omega \}$$ is a set, but with this latter part I have no problems, so I won't go into it.)

Intuitively I see how $\omega + n$, for any particular $n$, is defined: you just iterate with the successor function $s$ to obtain that $\omega + n$ is a set for each $n \in \omega$.

Now I was thinking about what the expression "$F : \omega \to V:n \mapsto \omega + n$" in ZFC means, i.e., which formula of the language of set theory corresponds to it.

I think it is the following.

"$F : \omega \to V : n \mapsto \omega + n$" is an abbreviation for the formula

"$F : \omega \to V$ is a function" $\wedge$ $[ \forall n \in \omega \, ( n , \omega + n ) \in F ]$.

Here "$F : \omega \to V$ is a function" is an abbreviation for

"$F$ is a function" $\wedge$ $\mbox{dom} ( F ) = \omega$ $\wedge$ $\mbox{range} (F) \subseteq V$,

where "$F$ is a function" and $\mbox{dom} (F) \subseteq \omega$ are of course itself again abbreviations (I won't give them here for reasons of brevity), and

$\mbox{range} ( F ) \subseteq V$ is an abbreviation for $\forall y \, ( \exists x \, (x,y) \in F \rightarrow y = y )$. (Which is a always true, so in retrospect I may as well had left this part out.)

So far so good, I guess.

But what about the expression $\forall n \in \omega \, ( n , \omega + n ) \in F$?

My 'problem' here is the $\omega + n$ in the formula. How can I express this? I've been thinking and searching for references about this for quite a while but I still haven't found a satisfactory answer.

-
Why not just $F = \{ ( x , y ) : x \in \omega \land y = \omega + x \}$? –  Andrew Salmon Mar 9 at 7:15
Yes, that's the same definition of $F$ that I gave. But the point is: how to express $y = \omega + x$? –  Elisheva Mar 9 at 7:16
They're taken from a recursive definition. You use transfinite recursion to define $+$ for ordinals. –  Andrew Salmon Mar 9 at 7:18
Okay. Is there no way to avoid transfinite recursion for this? I wanted to keep it as simple as possible. What kind of axioms do we need for that? –  Elisheva Mar 9 at 7:21
@Andreas: Taking my rare "over six hours sleep". –  Asaf Karagila Mar 9 at 10:16

Note that "$\omega + n$" is defined recursively according to

• $\omega + 0 = \omega$;
• $\omega + ( n + 1 ) = ( \omega + n ) + 1\;( = ( \omega + n ) \cup \{ \omega + n \} )$.

As the (class) function $\alpha \mapsto \alpha + 1$ is definable, it follows that there will be a formula in the language of set-theory that corresponds to $n \mapsto \omega + n$. This formula will not be at all simple, but basically says the following:

$\langle n , \alpha \rangle \in F$ iff either $n = 0$ and $\alpha = \omega$, or $0 < n < \omega$ and there is a function $f : n \to V$ such that $f(0) = \omega$ and $f(i+1) = f(i) + 1$ for all $i < n-1$ and $\alpha = f ( n-1 ) + 1$.

Note that there are a lot of abbreviations used in the above.

-
Thanks for you answer, I think I get it. –  Elisheva Mar 9 at 8:05