Which ordinals are proof-theoretic ordinals?

Question

Few months ago I have posted this question on MO, but I must admit that at the time, admittedly, I had no idea on how technical proof-theoretic considerations can be. I have decided to revise this question, and I thought that asking a new question is a better option that rewriting the old one (especially given that the other one has a partial answer to old question).

Given theory $T$ and recursive relation $\prec$, we say that $T$ proves $\prec$ to be well-ordered if $T$ proves that $\prec$ is a linear order and that $\forall X:((\forall n\prec m:n\in X)\Rightarrow n\in X)\Rightarrow\forall n:n\in X$.

We define proof-theoretic ordinal (PTO) of $T$ to be supremum of order types of relations which $T$ proves to be well-order.

Which recursive ordinals are PTOs of some theory extending $RCA_0$? How about theories extending $ACA_0$?

Side question: What is the PTO of theory $ACA_0+$ "$\varepsilon_0$ is well-ordered", where with $\varepsilon_0$ I mean a canonical well-ordering with order type $\varepsilon_0$?

Answer 1

If $\alpha$ is a reasonable presentation of a computable ordinal then the proof-theoretic ordinal of $ACA_0+\alpha$ is well-ordered is the smallest $\epsilon$ number $>\alpha$. (There's a proof of the upper bound in Epsilon substitution method for $ID_1(\Pi^0_1\vee\Sigma^0_1)$ by Arai, though there are probably simpler proofs out there. The lower bound follows by relativizing the usual argument to the representation of $\alpha$.)

It follows that every computable $\epsilon$-number is the proof-theoretic ordinal of an extension of $ACA_0$. For weird theories, the notion of a proof-theoretic ordinal may not be well-defined (it may depend which definition you use), but if $T$ extends $ACA_0$ and proves the well-foundedness of an ordering of order-type $\alpha$, it also proves the well-foundedness of an ordering of order-type $\omega^\alpha$: there's apparently a proof in Proof theory and logical complexity by Girard, and some related exposition in the papers by Marcone-Montalbon and by Rathjen and his students where they prove similar theorems for order ordinal operaions. That basically shows that the computable $\epsilon$-numbers are the only proof-theoretic ordinals over $ACA_0$.