Does ATR0 prove existence of uncomputable well-ordering?

Question

I recently came across this webpage that mentions a system ATR0 + "every ordinal is recursive". I am not sure what exactly that means, but anyway I tried and failed to construct an uncomputable well-ordering within ATR0. Basically, I see no way to construct the set of programs that compute well-orderings, so it seems that in this sense ATR0 cannot prove the existence of an uncomputable well-ordering. Is this true, and if so, why? I am unable to find a reference, presumably because I do not know the right search terms.

Answer 1

EDIT: Per Andreas' comment below, there's a slight issue around what "computable well-ordering" means. There are two possible interpretations: a well-ordering of $\mathbb{N}$ which is not computable, or a well-ordering of $\mathbb{N}$ which is not isomorphic to any computable well-ordering. I assume that the latter is meant, since "There is a non-computable set" implies that there is a well-ordering of $\mathbb{N}$ which is not itself computable.

This is a situation where the term "(non)computable ordinal" comes into play. It's not exactly universal, but generally when people talk about a "noncomputable well-ordering" they're referring to an actual well-ordering of $\mathbb{N}$ which is noncomputable, whereas "noncomputable ordinal" often means a well-ordering of $\mathbb{N}$ not isomorphic to any computable one. For this reason, I'll talk below about ordinals rather than well-orderings, to emphasize the meaning of computability here.

---

ATR$_0$ cannot in fact prove the existence of a non-recursive ordinal; this is because, over ATR$_0$, the existence of a non-recursive ordinal implies the existence of Kleene's $\mathcal{O}$.

Roughly speaking, suppose $\alpha$ is non-recursive. Then for $L_e$ a computable ordering, we have that $L_e$ is an ordinal iff there is an embedding of $L_e$ into $\alpha$ - this uses the fact that all ordinals are comparable, which is provable in ATR$_0$. Together with the usual $\Pi^1_1$ definition of ordinals, this gives a $\Delta^1_1$ definition of $\mathcal{O}$, and ATR$_0$ implies $\Delta^1_1$-CA$_0$.

So any model of ATR$_0$ + "There is a non-recursive ordinal" satisfies "$\mathcal{O}$ exists" (basically: lightface $\Pi^1_1$-comprehension). But the usual proof that ATR$_0$ is strictly weaker than $\Pi^1_1$-CA$_0$ builds a model of ATR$_0$ which doesn't satisfy "$\mathcal{O}$ exists." So we're done.

---

Incidentally, the standard reference on reverse math is Simpson's book; this is especially true in my opinion for results on systems stronger than ACA$_0$ (Hirschfeldt's book treats systems up to and including ACA$_0$, but doesn't go past there). The material on $\beta$-models especially is relevant.