# Equivalent statement of transfinite/ordinal recursion

I am trying to prove that the "standard" statement of transfinite/ordinal recursion:

"Suppose $G$ is a definite operation on partial functions on ordinals. Then there is a unique definite operation $F$ on ordinals satisfying $F(\alpha) = G(F|_\alpha)$ for all ordinals $\alpha$."

implies this alternate statement:

"Suppose $G_1$ is a set, $G_2$ is a definite operation on sets, and $G_3$ is a definite operation on partial functions on ordinals. Then there is a unique definite operation $F$ on ordinals such that $F(0) = G_1$, $F(S(\alpha)) = G_2(F(\alpha))$ for all ordinals $\alpha$, and for all limit ordinals $\alpha > 0$, $F(\alpha) = G_3(F|_\alpha)$."

Obviously I need to construct a $G$ that "encodes" $G_1$, $G_2$ and $G_3$, but I'm not sure what I can do while ensuring that the resulting $G$ is definite. For example, can I define $G$ to send the empty function to $G_1$, but behave like $G_3$ on non-empty sets? I think this would be wrong though, because then I'm unable to "build $G_2$ into $G$". I'd be very grateful for any assistance.

-
I don't really have the time to sit and write an answer, but I do wish to remark that $0$ is not a limit ordinal, so in the alternative statement pointing out "for all limit ordinals $\alpha>0$ ..." is redundant. – Asaf Karagila Sep 26 '12 at 8:48
My definition of "limit ordinal" is "not a successor ordinal". 0 is certainly not a successor ordinal, so why do you claim it's not a limit ordinal? – dx7hymcxnpq Sep 26 '12 at 8:54
Because the common definition of a limit ordinal is not just "not a successor", but rather "a non-zero ordinal which is not a successor". In a lot of ways limit ordinals play a much more important role in set theory (e.g. they form clubs and stationary sets) and zero has its own unique properties to begin with. So it is common to classify three kinds of ordinals: zero; successors; and limit ordinals. – Asaf Karagila Sep 26 '12 at 8:57
I agree with @Asaf: the term limit ordinal generally excludes $0$, because it’s understood literally: the limit ordinals are precisely those that are the limit of the smaller ordinals. (Admittedly there are times when this usage is mildly inconvenient, and would rather have a short term meaning non-successor ordinal.) – Brian M. Scott Sep 26 '12 at 9:05

There’s nothing wrong with building $G$ by cases, so to speak. Here’s a start:
\begin{align*} \Big(G(x)=y\Big)&\leftrightarrow\Big(x=0\land y=G_1\Big)\\ &\lor\Big(\exists\alpha\in\mathbf{ON}\big(x\text{ is a function}\land\operatorname{dom}x=\alpha\land\operatorname{cf}\alpha\ge\omega\land y=G_3(x)\big)\Big)\\ &\lor \dots\;; \end{align*}
Thanks. I don't understand how we can have "$x = \alpha \land x \text{ is a function}$" in your comment. Can you clarify? Also, what is "cf"? I think I'm getting closer; I want to define $G(x) = G_1$ if $x$ is the empty function, $G(x) = G_2(\alpha)$ if $x = F|_{S(\alpha)}$ for some ordinal $\alpha$, and $G(x) = G_3(x)$ if $x = F|_{\alpha}$ for some limit ordinal $\alpha$. Is there a more formal way to say this? – dx7hymcxnpq Sep 26 '12 at 8:53
@mlbaker: Ignore $x=\alpha$: it was left over from a previous version, and I simply forgot to remove it. (I’ve now done so.) $\operatorname{cf}\alpha$ is the cofinality of $\alpha$; if you’ve not yet learned about cofinality, substitute $\alpha\text{ is a limit ordinal}$ for $\operatorname{cf}\alpha\ge\omega$. Your definition cannot refer to $F$: that’s the object that you’re trying to construct. That’s why my $G_3$ clause doesn’t talk about $F\upharpoonright\alpha$, but about an arbitrary function with domain $\alpha$. The way that I’m suggesting is formal, with the understanding ... – Brian M. Scott Sep 26 '12 at 8:59
Ah, of course. So how about this for the third clause? $\exists \alpha \in \mathbf{ON}(x \text{ is a function} \land \operatorname{dom} x = S(\alpha) \land y = G_2(x(\alpha)))$. – dx7hymcxnpq Sep 26 '12 at 9:02