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.

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? • 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. – Emil Jeřábek Oct 27 '14 at 21:59 • Yes, you are right. I actually had induction up to$\epsilon_0$in mind. I edited the question. – Wojowu Oct 27 '14 at 22:06 1 Answer 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.

• 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. – Wojowu Oct 28 '14 at 9:54