Jtdylktuy

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.

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.