Proof-theoretic ordinals: inevitable consistency?

Question

There are various different notions of the proof-theoretic ordinal of a theory; most of these are "notation-dependent" in that they're only nontrivial once we restrict attention to a class of "natural" notations. There are, however, ways to attack this in a notation-independent way (e.g. the supremum of the ordinals which have notations which the theory proves induction along).

I'm interested in the following naive variant on the (notation-dependent) definition "The least ordinal such that induction along that ordinal proves the consistency of the theory:"

By "notation" below I mean "element of Kleene's $\mathcal{O}$," but if some other notion of notation would be preferable feel free to use it instead - if (1) it is precisely defined (= no reference to "naturality" etc. and (2) every computable ordinal has at least one notation (= no cheating by only going up partway).

---

Suppose $T$ is an "appropriate" theory - that is, recursively axiomatizable, fully sound, interpreting PA, and (for simplicity) in the language of second-order arithmetic (so we can talk directly about well-foundedness).

The inevitable consistency ordinal of $T$ is the least ordinal $\alpha$ such that for every notation $n$ for $\alpha$, RCA$_0$ + "The ordering defined by $n$ is well-founded" proves the consistency of $T$.

A couple comments:

• Per the second section of this answer, if we replace "every" by "some" we always get $\omega$; the point of inevitability is that there's no way to avoid getting consistency, no matter how we describe $\alpha$ to RCA$_0$ we wind up getting Con$(T)$.)*

• I'm replacing the usual base theory PRA with the stronger theory RCA$_0$ so I don't have to worry about low-level shenanigans; I'm really not interested in optimal calculations right now, just coarse behavior.

---

While inevitable consistency is a fully notation-independent notation, it's not clear to me that the corresponding ordinal always exists - to put it mildly!

My question is:

Does the inevitable consistency ordinal of ACA$_0$ (which is conservative over PA) exist?

If the answer is "yes," natural follow-up questions include:

• Is it equal to $\epsilon_0$ (or at least close to that)?

• Does such an ordinal always exist for an appropriate $T$?

  • Note that the ordinal described in the parenthetical of the first paragraph of this question does in fact always exist, by $\Sigma^1_1$ bounding, so this isn't as ridiculous as it may sound.

One unconditional further question which occurs to me is:

• How "coarse" can inevitable consistency be - e.g. is there an obvious reason why, if the inevitable consistency ordinal for $\Pi^1_1$-CA$_0$ (say) exists, then it must be different from that of ACA$_0$?

Answer 1

The ineventable consistency ordinals do not exist for all the computably axiomatizable extensions of $\mathsf{RCA}_0$. Indeed, for any given notation system $\alpha$ I'll construct a notation system $\alpha^*$ such that $\alpha$ and $\alpha^*$ are notations for the same ordinal and $\mathsf{RCA_0}\vdash \lnot \mathsf{Con}(\mathsf{RCA}_0)\to\mathsf{WF}(\alpha^*)$. By Gödel's second incompleteness theorem the theory $\mathsf{RCA}_0+\lnot\mathsf{Con}(\mathsf{RCA}_0)$ is consistent. And hence we would have consistency of $\mathsf{RCA_0}+\lnot\mathsf{Con}(\mathsf{RCA}_0)+\mathsf{WF}(\alpha^*)$. Which of course mean that $\mathsf{RCA}_0+\mathsf{WF}(\alpha^*)$ doesn't prove $\mathsf{Con}(T)$, for any computably axiomatizable extension $T$ of $\mathsf{RCA}_0$.

Now I'll construct $\alpha^*$. Let us work in $\mathsf{RCA}_0$. For each $n$ we consider the finite binary relation $\alpha\upharpoonright_n$ that consists of all $\beta<n$ such that the witness for the $\Sigma_1$ sentence $\beta<_{\mathcal{O}^*}\alpha$ is less than $n$ and $\beta_1<_{\alpha\upharpoonright_n} \beta_2$ if the witness for the $\Sigma_1$ sentence $\beta_1<_{\mathcal{O}^*}\beta_2$ is less than $n$. Let $\alpha^*_n$ to be $\alpha\upharpoonright_m$, where $m$ is the greatest number $\le n$ such that there are no proofs of contradiction in $\mathsf{RCA}_0$ of the length $<m$ and the binary relation $\alpha\upharpoonright_m$ is well-founded. Clearly, $\alpha^*_n$ constitute uniformly computable sequence of binary relations such that $\alpha^*_n\subseteq \alpha^*_{n'}$, for $n\le n'$. We define $\alpha^*$ to be an element of $\mathcal{O}^*$ such that the cone below it is isomorphic to $\bigcup_{n\in \omega} \alpha^*_n$ and each $\beta<_{\mathcal{O}^*}\alpha^{\star}$ is successor iff it was successor in $\alpha$. Observe that from the assumptions that $\mathsf{RCA}_0$ is consistent and that $\alpha$ is well-founded it follows that $\alpha\upharpoonright_ n=\alpha^*_n$, for all $n$ and hence that $\alpha^*$ is isomorphic to $\alpha$ and is an element of $\mathcal{O}$. On the other hand from the assumption that $\lnot\mathsf{Con}(\mathsf{RCA}_0)$ we conclude that $\alpha^*$ is some $\alpha^*_n$ and hence is a finite well-founded order.

Note that this ineventable ordinals wouldn't exist even if we would define it as

the least ordinal $\alpha$ such that for every notation $n$ for $\alpha$, $\mathsf{RCA}_0+\text{full scheme of transfinite induction over the order defined by $n$}$ proves the consistency of T.

This was proved by Beklemeishev [1]. The argument above essentially is based on similar ideas, but for a simpler case.

[1] Beklemishev, L.D. (2000): Another pathological well-ordering. In S. Buss et al., editors, Logic Colloquium '98 Proceedings, Lecture Notes in Logic 13, A.K.Peters, Ltd., Natick MA, 105-108.