A question about ordinal analysis

Question

I have several questions related to ordinal analysis.

According to [1], 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?

Answer 1

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.

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.