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 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.2012-09-26
  • 0
    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?2012-09-26
  • 2
    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.2012-09-26
  • 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
    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?2012-09-26
  • 0
    @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 ...2012-09-26
  • 0
    ... that the items specified verbally can in principle be written out entirely in the formal language of set theory.2012-09-26
  • 0
    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)))$.2012-09-26
  • 0
    @mlbaker: Looks good to me.2012-09-26