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.
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*}$$
you just have to build in the third disjunct, the one that handles successor ordinals.