Skip to main content
4 of 8
added 650 characters in body
Wojowu
  • 28.2k
  • 3
  • 103
  • 185

Which ordinals can be proof-theoretic ordinals of a reasonable theory?

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?

Wojowu
  • 28.2k
  • 3
  • 103
  • 185