When talking to a friend recently he asked a question - are there any reasonable first-order theories which have proof theoretic ordinal equal to small or large Veblen ordinal? I have then extended his question broadly - which ordinals can be proof-theoretic ordinals of any "reasonable" theory, where by "reasonable" I suggested we should mean "extending PA", though this can be discussed. (Edit: it seems convinient to be able to work with second-order theories, so instead we can think of "reasonable" as extending $\sf ACA_0$)

Another, related question is the following: what is the proof-theoretic ordinal of theory PA+axiom schema asserting transfinite induction holds up to $\varepsilon_0$? I think it might be $\varepsilon_1$, but I can't be sure.

Thanks in advance for feedback!

EDIT: I have decided to state an alternative version of this question, which will hopefully be less ambiguous.

Let our base system be $\sf ACA_0$. Suppose that we add to this system a statement "ordinal $\alpha$ is well-founded", expressed as second order predicate. Now we know that proof-theoretic ordinal of this theory will be greater than $\alpha$. Let's call ordinal $\gamma$ bounding if, whenever $\alpha<\gamma$, then PTO of $\sf ACA_0$+"$\alpha$ is well-founded" is also $<\gamma$. Then my question is, which recursive ordinals are bounding? We know that $\varepsilon_0$ is bounding, but what is the least bounding ordinal above it?

EDIT2: I've recently realized that even second order theory can't really just talk about $\varepsilon_0$ or pretty much any ordinal per se, but we need to represent the ordinal in a way (e.g. we could represent $\varepsilon_0$ as an ordering on numbers representing ordinals in Cantor's normal form). Because of this, there can be multiple ways to express ordinal, and some of them could also hide some complexity (e.g. we can have an ordering which is well-ordered with order type $\varepsilon_0$ only if Kruskal's tree theorem holds). Because of this, we can have statement "$\alpha$ is well-founded$ hide an information about well-ordering of any recursive ordinal. Is that true?

  • 2
    $\begingroup$ See mathoverflow.net/questions/123713 for a related question. In particular, there is no such thing as PA + “$\varepsilon_0$ is well-founded”, as well-foundedness is a $\Pi^1_1$ property, so you need to be more precise. $\endgroup$ Commented Oct 27, 2014 at 21:59
  • $\begingroup$ Yes, you are right. I actually had induction up to $\epsilon_0$ in mind. I edited the question. $\endgroup$
    – Wojowu
    Commented Oct 27, 2014 at 22:06
  • $\begingroup$ Is $\varepsilon_0$ bounding? For example if $\alpha=\omega^\omega$, then the PTO of $\mathsf{ACA}_0$+"$\omega^\omega$ is well-founded" is $\varepsilon_0$, which is not less than $\varepsilon_0$. $\endgroup$
    – C7X
    Commented Jun 7 at 6:40
  • $\begingroup$ @C7X I'm uncertain what I meant 10 years ago but I think replacing it with "PTO of ... is $\leq\gamma$" would match what I was after. But then again by now I am aware this is very sensitive to how the well-orders are coded and just speaking of ordinals on their own doesn't make sense here, so I'm not sure how meaningful that question is. $\endgroup$
    – Wojowu
    Commented Jun 7 at 10:30

1 Answer 1


Regarding the small Veblen ordinal, Rathjen and Weiermann gave an analysis of theories in that range of strength in Proof-theoretic investigations of Kruskal's theorem. Working over a reasonable base theory ($ACA_0$, the second order version of Peano arithmetic), both the theory $ACA_0+$Kruskal's theorem and a somewhat technical theory ($ACA_0$ plus $\Pi^1_1$ reflection for $\Pi^1_2$-BI; $\Pi^1_2$-BI is induction along internally well-ordered sets for $\Pi^1_2$ formulas, and $\Pi^1_1$ reflection means that the statement itself doesn't hold, but all its $\Pi^1_1$ consequences do). (I'm not sure if any of their theories are exactly the large Veblen ordinal.)

The more general question seems too vague to answer. As the Rathjen and Weiermann article shows, there are an awful lot of reasonable-ish theories out there.

  • $\begingroup$ Thanks for the answer. From what I understand, ACA_0+Kruskal's theorem actually shows small Veblen ordinal well-founded, so its PTO would have to be strictly higher. I haven't read whole paper, so I might be wrong. $\endgroup$
    – Wojowu
    Commented Oct 28, 2014 at 9:54
  • $\begingroup$ This table dated 2018 from an unknown source does not seem to list the large veblen ordinal as a proof-theoretic ordinal of any well-known system. Do you know of one now, since it's been a few years after your answer here? =D $\endgroup$
    – user21820
    Commented May 13, 2020 at 6:03
  • $\begingroup$ @user21820: I'm not aware of any work trying to identify a theory precisely at that ordinal, nor a lot of current work on theories around it, so I doubt the situation has changed. $\endgroup$ Commented May 13, 2020 at 13:50
  • $\begingroup$ Alright thank you! $\endgroup$
    – user21820
    Commented May 13, 2020 at 16:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.