0
$\begingroup$

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.

  • 0
    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*.)2012-09-26

1 Answers 1

2

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.

  • 0
    @mlbaker: Looks good to me.2012-09-26