7
$\begingroup$

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$?

$\endgroup$
8
$\begingroup$

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$.

$\endgroup$
1
  • $\begingroup$ Thanks for these references. Unless someone else provides an answer regarding extensions of RCA_0, I am going to accept your answer. $\endgroup$ – Wojowu Jul 11 '15 at 19:24

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.