7
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.