I have several questions related to ordinal analysis.


According to [[1](https://ncatlab.org/nlab/show/ordinal+analysis)], here are the proof-theoretic ordinal of some well-known theories (using $|T|$ do denotate the proof-theoretic ordinal of $T$):


* $ |\text{ATR}\_0|=\Gamma\_0,|\text{ATR}|=\Gamma\_{\varepsilon\_0} $
* $ |\Pi^1\_0-\text{CA}\_0|=\varepsilon\_0,|\Pi^1\_0-\text{CA}|=\varepsilon\_{\varepsilon\_0}<\varphi(\varepsilon\_0,0)=|\Delta^1\_1-\text{CA}|$
* $|\Pi^1\_1-\text{CA}\_0|=|\Delta^1\_2-\text{CA}\_0|=\psi(\Omega\_\omega)$
* $|\Pi^1\_1-\text{CA}|=\psi(\Omega\_\omega\varepsilon\_0)<\psi(\Omega\_{\varepsilon\_0})=|\Delta^1\_2-\text{CA}|$


(Notice when there is a 0 subscript and when there isn't. Of course $\Pi^1\_0-\text{CA}\_0$ is $\text{ACA}\_0$.)


I have never seen $|\Delta^1\_1-\text{CA}\_0|$ mentioned anywhere, but seeing the $\Delta^1\_2$ case I suppose it has proof-theoretic ordinal $\varepsilon\_0$.


More generally the following equality seem a reasonable conjecture:
 $ |\Pi^1\_n-\text{CA}\_0| = |\Delta^1\_{n+1}-\text{CA}\_0| < |\Pi^1\_n-\text{CA}|<|\Delta^1\_{n+1}-\text{CA}| $ for all $n$. Does anybody has a proof or reference for this?


Also every time the 0 subscript is dropped, the ordinal $\varepsilon\_0$ appears in the proof-theoretic ordinal of the resulting theory. Is there a simple reason or intuition why this happens?



A question about ordinal analysis
First of all, note that we don't (yet) have ordinal analyses of subsystems of second order arithmetic beyond $\Pi^1\_2$-CA$\_0$.


Still, we can say something about the pattern you indicate using known results about these systems. A good reference is the book by Stephen G. Simpson: [Subsystems of Second Order Arithmetic](http://www.personal.psu.edu/t20/sosoa/).


There we find for instance:


* $\Delta^1\_{k+3}$-CA$\_0$ is a conservative extension of $\Pi^1\_{k+2}$-CA$\_0$ for $\Pi^1\_4$-sentences. (Cor. IX.4.12)
* $\Delta^1\_{k+2}$-CA proves the existence of a countable coded $\beta$-model of $\Pi^1\_{k+1}$-CA$\_0$. (Cor. VII.7.9)
* $\Pi^1\_{k+1}$-CA$\_0$ proves the existence of a countable coded $\beta$-model of $\Delta^1\_{k+1}$-CA$\_0$. (Cor. VII.7.9)


Finally, let me speculate a bit on your last question. I don't think there's a formal theorem to this effect. (At least not with current technology.) The subsystem $T$ without the subscript $0$ differs from $T\_0$ by adding full induction. When we have all the tools for an ordinal analysis of $T\_0$, we can often get one for $T$ by (in some sense) iterating our procedure for $T\_0$ along $\varepsilon\_0$ to do the cut-elimination with full induction. But it's not so straight-forward, as the exact steps differ widely in each case, for instance if collapsing is involved. Have a look at Pohlers' chapter on *Subsystems of set theory and second-order number theory* in the Handbook of Proof Theory. There you'll see some instances of this pattern, at least as far as the upper bounds are concerned.


Perhaps a more general statement could have been made using Girard's $\Pi^1\_n$-logic, but that's the realm of wild speculation on my part, and I don't think this was ever developed enough, particularly in connection with subsystems of second order arithmetic.


