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

Question

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

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.

¹Rathjen, Michael; Weiermann, Andreas, Proof-theoretic investigations on Kruskal’s theorem, Ann. Pure Appl. Logic 60, No. 1, 49-88 (1993). ZBL0786.03042.

Answer 2

Pakhomov and Walsh proved the following result:

Theorem. Let $\alpha$ be an ordinal notation. Then $|\mathbf{R}^\alpha_{\Pi^1_1}(\mathsf{ACA}_0)|_{\Pi^1_1}=\varepsilon_\alpha$.

Here $\mathbf{R}^\alpha_{\Pi^1_1}(T)$ is the '$\alpha$th iterate of $T$' defined by the fixed point lemma. (See Subsection 2.3 of Pakhomov-Walsh's Reflection ranks and ordinal analysis.) If every ordinal notation can have an ordertype of a recursive ordinal, then their theorem proves that every recursive epsilon number can be a proof-theoretic ordinal of a recursive sound extension of $\mathsf{ACA}_0$.

However, their result uses the notion of ordinal notation which is a special type of recursive well-ordering. I am unsure if every recursive ordinal is isomorphic to an ordinal notation. Thus let me give a different proof for the claim that every epsilon number can be a proof-theoretic ordinal for a sound recursive extension of $\mathsf{ACA}_0$.

The main ingredient of my argument is Aguilera-Pakhomov's $\Pi^1_2$-ordinal analysis for $\mathsf{ACA}_0$:

Theorem. (Aguilera-Pakhomov) $|\mathsf{ACA}_0|_{\Pi^1_2}=\varepsilon^+$, where $\varepsilon^+$ is a dilator returning the least epsilon number greater than the input (so $\varepsilon^+(\alpha)>\alpha$ is the epsilon number.)

A dilator is a continuous stable (i.e., preserving direct limits and pullbacks) functor from the category of ordinals to the same category. Dilators look like very large objects, but it is known that every dilator is determined by its restriction to the category of natural numbers with increasing maps. Hence we can say a given dilator is recursive or not by checking if there is a recursive set coding the restriction of the dilator to the category of natural numbers.

A proof-theoretic ordinal $|T|_{\Pi^1_1}$ encodes $\Pi^1_1$-consequences of $T$, and likewise, a proof-theoretic dilator $|T|_{\Pi^1_2}$ encodes a $\Pi^1_2$-consequence of $T$. If $T$ is recursive, then so is $|T|_{\Pi^1_2}$. Also, we understood $|T|_{\Pi^1_2}$ as a functor over the category of ordinals. But we can replace it with the category of well-orders, or even, linear orders. Hence the notion $|T|_{\Pi^1_2}(\alpha)$ makes sense for a general linear order $\alpha$, and $|T|_{\Pi^1_2}(\alpha)$ is recursive if $T$ and $\alpha$ are.

The following theorem gives an extensional description of a proof-theoretic dilator:

Theorem. (Aguilera-Pakhomov) Let $T$ be a $\Pi^1_2$-sound theory and $\alpha$ be a recursive linear order. Then $$|T|_{\Pi^1_2}(\alpha) = |T + \mathsf{WO}(\alpha)|_{\Pi^1_1}.$$

---

Now let $\alpha$ be a recursive epsilon number. Consider the theory $$T_\alpha = \mathsf{ACA}_0 + \{\mathsf{WO}(\alpha\upharpoonright \underline{n}) \mid n\in\operatorname{field}(\alpha)\},$$ where $\alpha\upharpoonright n$ is the initial segment of $\alpha$ given by $n$. ($\underline{n}$ is the numeral of value $n$.) Then $T_\alpha$ is recursive and sound.

Now let us claim that $|T_\alpha|_{\Pi^1_1} = \alpha$ as follows: By definition, we have $|T_\alpha|_{\Pi^1_1} \ge \alpha$. For the opposite direction, consider $$T_\alpha^{<m} = \mathsf{ACA}_0 + \{\mathsf{WO}(\alpha\upharpoonright \underline{n}) \mid n\in\operatorname{field}(\alpha),\ n<m\}.$$ Then $|T_\alpha|_{\Pi^1_1}=\sup_m |T_\alpha^{<m}|_{\Pi^1_1}$. Furthermore, if $\alpha\upharpoonright k$ has the largest ordertype among $\alpha\upharpoonright n$ for $n<m$, then $$|T_\alpha^{<m}|_{\Pi^1_1} = |\mathsf{ACA}_0 + \mathsf{WO}(\alpha\upharpoonright \underline{k})|_{\Pi^1_1} = \varepsilon^+(\alpha\upharpoonright k) \le \alpha.$$ Hence we have $|T_\alpha|_{\Pi^1_1} \le \alpha$.

Answer 3

$\newcommand{\bomega}{\boldsymbol\omega}$Given the definition of bounding ordinal in the post and the potential sensitivity to coding mentioned in edit 2, these seem to be two main ways to formalize boundedness:

• $\gamma$ is bounding if for all $\alpha<\gamma$, for all ordinal notations $\{e\}$ computing $\alpha$, we have $\vert\mathsf{ACA}_0+``\{e\}\text{ computes a well-order}"\vert_{sup}\leq\gamma$.
• $\gamma$ is bounding if for all $\alpha<\gamma$, there exists an ordinal notation $\{e\}$ computing $\alpha$ such that we have $\vert\mathsf{ACA}_0+``\{e\}\text{ computes a well-order}"\vert_{sup}\leq\gamma$.

Edit Jun 29: By Hanul Jeon's answer, these are equivalent.

(Here an ordinal notation is a computable function computing the composition of the indicator function of a well-ordering with an unpairing function.) Taking either definition of boundingness, a result is possible which is relevant to the question in your edit: all bounding ordinals are epsilon ordinals.

---

Write $\prec_{\{e\}}$ for the well-ordering computed by a computable function $\{e\}$, $\mathrm{ot}(\prec)$ for the order type of a well-ordering $\prec$, and write $\mathrm{fld}(\prec)$ for the union of $\prec$'s domain and range.

The core of the following argument is Girard's equivalence result, and then three corollaries quickly follow.

Lemma: Let $T$ be a theory containing $\mathsf{ACA}_0$ and $\alpha$ be an ordinal. If there is an ordinal notation $\{e\}$ with order type $\alpha$ such that $T$ proves $\{e\}$ computes a well-order, then $\vert T\vert_{sup}\geq\omega^\alpha$.

Proof: Let $T$, $\alpha$, and $\{e\}$ be as given. Girard showed that arithmetical comprehension is equivalent over $\mathsf{RCA}_0$ to "for all linear orders $\prec$, if $\prec$ is well-founded then $\bomega^\prec$ is well-founded". (Marcone, Montalbán, "The Veblen functions for computability theorists", 2010). Here $\bomega^\prec$ is a kind of linear order exponentiation, briefly $\bomega^\prec$ is the lexicographic ordering on monotonically-$\prec$-decreasing finite tuples of members of $\mathrm{fld}(\prec)$. (The definition with detail is on page 4 of the previous source.)

Since $\prec_{\{e\}}$ is computable and $\bomega^{\prec_{\{e\}}}$ is essentially a lexicographic ordering on a computable set, $\bomega^{\prec_{\{e\}}}$ is computable. By looking at the Cantor normal form of $\mathrm{ot}(\prec_{\{e\}})$, the order type of $\bomega^{\prec_{\{e\}}}$ is $\omega^{\mathrm{ot}(\prec_{\{e\}})}$, and since $\mathrm{ot}(\prec_{\{e\}})=\alpha$, we have $\mathrm{ot}(\bomega^{\prec_{\{e\}}})=\omega^\alpha$. Let $\{d\}$ be an ordinal notation that computes $\bomega^{\prec_{\{e\}}}$. Thus we have an ordinal notation $\{d\}$ that computes the ordinal $\omega^\alpha$, and $T$ proves that it computes a well-order. Thus $\vert T\vert_{sup}\geq\omega^\alpha$. $\square$

Corollary 1: If $T$ contains $\mathsf{ACA}_0$, its PTO is an epsilon ordinal.

Proof: Let $\gamma=\vert T\vert_{sup}$, and $\alpha<\gamma$ be an arbitary ordinal. Let $\{e\}$ be an arbitrary ordinal notation of order type $\alpha$ that $T$ proves computes a well-order. By the lemma, we have $\vert T\vert_{sup}\geq\omega^\alpha$, i.e. $\gamma\geq\omega^\alpha$. As $\alpha<\gamma$ was arbitrary, $\gamma$ is an epsilon ordinal. $\square$

Corollary 2: Any bounding ordinal (using the first definition) is an epsilon ordinal.

Proof: Assume $\gamma$ is a bounding ordinal, using the first definition. Choose an arbitrary ordinal $\alpha<\gamma$ and an arbitrary ordinal notation $\{e\}$ computing $\alpha$. Then $\vert\mathsf{ACA}_0+``\{e\}\text{ computes a well-order}"\vert_{sup}\geq\omega^\alpha$, and by boundingness this ordinal is $\leq\gamma$. As $\alpha<\gamma$ was arbitrary, we have shown that for any $\alpha<\gamma$ we have $\omega^\alpha\leq\gamma$, so $\gamma$ must be an epsilon ordinal. $\square$

Corollary 3: Any bounding ordinal (using the second definition) is an epsilon ordinal.

Proof: Assume $\gamma$ is a bounding ordinal, using the second definition. Choose an arbitrary ordinal $\alpha<\gamma$ and an ordinal notation $\{e\}$ computing $\alpha$ such that $\vert\mathsf{ACA}_0+\{e\}\text{ computes a well-order}\vert_{sup}\leq\gamma$. Then $\vert\mathsf{ACA}_0+``\{e\}\text{ computes a well-order}"\vert_{sup}\geq\omega^\alpha$, and by boundingness this ordinal is $\leq\gamma$. As $\alpha<\gamma$ was arbitrary, we have shown that for any $\alpha<\gamma$ we have $\omega^\alpha\leq\gamma$, so $\gamma$ must be an epsilon ordinal. $\square$

---

I am not sure how to show that any particular ordinal greater than $\varepsilon_0$ is limiting using these definitions, or even if $\varepsilon_0$ is limiting using the first definition. For these problems it suffices to show that there is no pathological computable well-ordering $\prec$ with $\mathrm{ot}(\prec)$ less than a desired $\gamma$ such that well-foundedness of $\prec$ implies well-foundedness of a computable well-ordering $\prec'$ with much higher order type. I have been unable to produce such counterexamples well-ordering $\prec$, and also unable to prove one does not exist. Maybe something in the spirit of the "Strong statements from small ordinals" paragraph of Dmytro Taranovsky's answer to MO question #432470 would help with constructing such a $\prec$, but I am unable to extend Taranovsky's work all the way up to $\Pi^1_1$ sentences, like "$\prec'$ is a well-ordering". I have also considered the Kleene-Brouwer ordering on a tree searching for an infinite decreasing sequence in $\prec'$, but was unable to show that it would have small order type.