Transfinite recursion to construct a function on ordinals

Question

I am asked to use transfinite recursion to show that there is a function $F:ON \to V$ (here $ON$ denote the class of ordinals and $V$ the class of sets) that satisfies:

1. $F(0) = 0$
2. $F(\lambda) = \lambda$ whenever $\lambda$ is a limit ordinal.
3. $F(\mathcal{S}(\lambda)) = \mathcal{S}(\lambda)$ whenever $\lambda$ is a limit ordinal or if $\lambda = 0$.
4. $F(\alpha+2) = F(\alpha) + F(\alpha+1)$ for all odinals $\alpha$.

I understand that I must construct a function $G: V\to V$ so that when restricted to $ON$, I get the properties above. I am unable to explicitly construct such a function that will yield the property 4 above.

Edited:

After asking this question I was pointed out that the transfinite recursion theorem (specifically the the notation $F(\alpha) = G(F\upharpoonright \alpha)$) gives a big hint on how to find the class function $G$ on $V$.

Specifically if $F(\alpha) = y$ then one must also have that $G(x) = y$ where $x = F\upharpoonright \alpha$. So $G(x) = y$ for a function $x$ whose domain is $\alpha$ (because $x = F\upharpoonright \alpha$) and for any $\beta \in \text{dom}(x) = \alpha$ we must also have that $F(\beta) = x(\beta)$.

With this it is easy to figure out that the desired $F$ is given by applying transfinite recursion theorem to the function $G:V\to V$, given by

$G(x) = \begin{cases} \text{dom}(x) & \text{ if } x \text{ is a function, } \text{dom}(x) \text{ is a limit ordinal or } 0 \\ \text{dom}(x) & \text{ if } x \text{ is a function, } \text{dom}(x) = \mathcal{S}(\lambda) \text{ for } \lambda = 0 \text{ or } \lambda \text{ is a limit ordinal.}\\ x(\alpha) + x(\mathcal{S}(\alpha)) & \text{ if } x \text{ is a function, } \text{dom}(x) = \mathcal{S}(\mathcal{S}(\alpha)) \text{ for some ordinal } \alpha\\ 0 & \text{ if } x \text{ is not a function or} \text{ if } x \text{ is a function but } \text{dom}(x) \text{ is not an ordinal.} \end{cases}$

The proposed $G$ is a class function because each of the expressions in the definition of $G$ such as "$x$ is a function", "$\text{dom}(x)$ is an ordinal" etc can be captured by formulas in the language of set theory

Answer 1

Use transfinite recursion to define the auxiliary function $G:\alpha\mapsto\langle F(\alpha),F(\alpha+1)\rangle$. Then define $F(\alpha)$ as the first component of the ordered pair $G(\alpha)$.

Answer 2

This can be done without using definition by transfinite recursion; ordinary recursion on the natural numbers is all that's needed.

Define $f(n)$ for $n<\omega$ by using ordinary recursion:

$$f(n) = \begin{cases} 0, & \text{if }n=0, \newline 1, & \text{if }n=1, \newline f(n-2)+f(n-1), & \text{otherwise.}\newline \end{cases}$$ (This is just the usual definition of the Fibonacci numbers.)

Now you can define $F(\alpha)$ for any ordinal $\alpha$ explicitly, as follows:

$$F(\alpha) = \begin{cases} f(\alpha), & \text{if }\alpha<\omega,\newline \alpha, & \text{if }\alpha\text{ is a limit ordinal,}\newline \lambda\,f(n+1)+1, &\text{if }\alpha=\lambda+n\text{, where }\lambda\text{ is a limit ordinal and }0 < n < \omega.\newline \end{cases}$$

You can verify that $F$ has the required properties.