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?


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.

| cite | improve this answer | |

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.