A theory which seems to have proof-theoretic ordinal $\omega_1^{CK}$

Question

I'm trying to understand proof-theoretic ordinals, and mistakenly "proved" there's a sound recursive theory of arithmetic with proof-theoretic ordinal $\omega_1^{CK}.$ That's impossible, so where does this go wrong?

"Proof:" Fix a recursive ordering $<_H$ on $\omega$ of length $\omega_1^{CK}(1+\eta),$ $\eta$ the order type of the rationals, with each nonempty hyperarithmetic set having a $<_H$-minimal element. Let $<_n$ be the initial segment of $<_H$ below $n.$ Then $<_n$ is a recursive ordering. Call $n$ $\textit{good}$ if the theory $S_n:=Z_2+``<_n$ is well-founded$"$ is arithmetically sound.

The set of good $n$ is hyperarithmetic and contains the well-founded part of $<_H,$ so there is some $n^*$ which is good and lies in the ill-founded part of $<_H.$ Then $T=$ PA $+``S_{n^*}$ is arithmetically sound$"$ is sound and recursive. Notice that for each $\alpha<\omega_1^{CK},$ there is $n$ such that $<_n$ is isomorphic to $\alpha,$ and $T$ proves $<_n$-induction. So $T$ is as desired.

Answer 1

Having read this post from Dmytro (https://mathoverflow.net/a/278615/109573), I think the answer here is that proof-theoretic ordinals are best defined for $\Pi_1^1$-sound theories which interpret a weak second order arithmetic (e.g. ACA$_0$). While we can reasonably assign weak first order theories (e.g. subsystems of PA) proof-theoretic ordinals based on how much induction they prove, this quickly becomes problematic.

For example, one might want to assign PA $+ \epsilon_0$-induction a proof-theoretic ordinal greater than $\epsilon_0.$ But then we would expect the second-order theory ACA$_0$ + arithmetic $\epsilon_0$-induction to have at least as high of a proof-theoretic ordinal, even though, if I'm not mistaken, this theory does not prove the well-foundedness of $\epsilon_0$ (at the very least, it's clear ACA$_0$ + arithmetic $\alpha$-induction does not prove well-foundedness of $\alpha$ for arbitrary recursive ordinals $\alpha$). So strong theories of first-order arithmetic probably don't have a clear proof-theoretic ordinal.