Equivalent definitions of $\omega_1^{\mathrm{CK}}$

computabilityset-theory

This is perhaps a somewhat tedious and technical question, but I've seen two definitions of $\omega_1^{\mathrm{CK}}$ (one from order-types and one from Kleene's $\mathcal{O}$), and I'm not immediately seeing why they should be equivalent. To be more specific, these are the definitions I'm working with: the first is the following.

An ordinal $\alpha$ is recursive iff there is some recursive $R\subseteq\omega\times\omega$ which has order-type $\alpha$. We define $\omega_1^{\mathrm{CK}}$ to be the supremum of all recursive ordinals.

The second is the following with whatever your favorite coding is:

The set of ordinal notations below is $\mathcal{O}$ defined as follows:

  • $0$ is an ordinal notation for $0$,
  • If $n$ is an ordinal notation for $\nu_n$, then $\mathrm{code}(0,n)$ is an ordinal notation for $\nu_n+1$,
  • If $P$ is the code of a program computing the map $k\mapsto n_k\in \mathcal{O}$ where $n_k$ is an ordinal notation for $\nu_k$, then $\mathrm{code}(1,P)$ is an ordinal notation for $\sup_{k<\omega}\nu_{n_k}$.

We define $\omega_1^{\mathrm{CK}}$ to be the supremum of ordinals with ordinal notations in $\mathcal{O}$.

In trying to prove the two definitions equivalent, it's not obvious to me how the limit stage should work. It seems to me like the inductive hypothesis wouldn't be enough, but it's not clear to me how one can strengthen it. In particular (going from the $\mathcal{O}$ characterization to the order-type characterization), if $n=\mathrm{code}(1,P)$ with $P$ computing $k\mapsto n_k$, inductively we get witnesses $R_k$ of order-type $\nu_{n_k}$. We might try to get a representative $R$ of order-type, e.g., $\sum_{k<\omega} \nu_{n_k}$ and then cut off at an initial segment to get one for $\sup_{k<\omega}\nu_{n_k}$. But to do any of this, we need the map $k\mapsto R_k$ (or rather to the program computing $R_k$) to be computable.

Basically, it's not clear to me why there could be a computable map $n\mapsto P_n$ where (if $n\in\mathcal{O}$) $P_n$ is a program computing an $R_n\subseteq\omega\times\omega$ of order-type $\nu_n$.

Best Answer

This is Theorem $4.4$ in Sacks' book Higher recursion theory (see here).

The "notations-to-relations" bit - which you ask about in particular - is a cute application of effective transfinite recursion:

(ETR) Suppose $\triangleleft$ is a wellfounded relation on $D\subseteq\omega$, and $I:\omega\rightarrow\omega$ is a recursive function. If for all $e<\omega$ and $x\in D$ we have $$[\forall y\triangleleft x(\varphi_e(y)\downarrow)]\implies\varphi_{I(e)}(x)\downarrow,$$ then there is some $c$ with $\forall x\in D(\varphi_c(x)\downarrow)$ and $\varphi_c\simeq\varphi_{I(c)}$.

This is Theorem $3.2$ in Sacks. A key point here is that $\triangleleft$ need not be recursive, and so in particular ETR applies to $<_\mathcal{O}$. This is a very slippery point, and worth meditating over (that's more-or-less a direct quote from Ted Slaman, IIRC).

The relevant application of ETR is then Theorem $3.5$. Informally speaking, the way the induction hypothesis is strengthened here is by adding a uniformity requirement, namely that we have a recursive procedure for passing from notations below the current notation to corresponding recursive relations. This is captured by the "$I$-part" of ETR: intuitively, $\varphi_{I(e)}(x)$ starts by assuming that $\varphi_e$ is in fact a way of finding relations corresponding to notations $<_\mathcal{O}x$. A fixed point for $I$ which is defined on all of $\mathcal{O}$ then amounts to such a correspondence which "keeps working" as long as it has "worked so far" - and by well-foundedness, this means it works everywhere.

That said, there is a technical subtlety here in the "relations-to-notations" direction. There is (Lemma $4.3$) a recursive $f$ such that for all $e$, if $R_e$ is well-founded then $f(e)\in\mathcal{O}$ and $\vert R_e\vert\le\vert f(e)\vert$ (I'm using two meanings of "$\vert\cdot\vert$" here, following Sacks). However, we cannot replace that "$\le$" with a "$=$" - there's always some unavoidable "overshooting" when we try to go from a recursive well-ordering to a corresponding notation.

It's also worth noting that there yet a third definition of $\omega_1^{CK}$, of genuinely different character (I'm not counting "the least non-hyperarithmetic ordinal" here, since it's too similar):

$\omega_1^{CK}$ is the smallest admissible ordinal $>\omega$, that is, the smallest ordinal $\alpha$ such that $L_\alpha\models KP$ and $\alpha>\omega$.

This may look like a very technical property at first, but it's extremely useful; it's also treated in Sacks' book. The two styles of definition ("least nonrecursive," "first admissible") relativize in interesting ways: we can talk about the least ordinal not recursive relative to an oracle, and we can talk about the $\eta$th admissible ordinal $>\omega$. The connection between the two notions in general is due to Sacks, although it has subtleties.

Related Question