# Proof-theoretic ordinals: inevitable consistency?

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$$.

• 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$$?
• The computability-theory and reverse-mathematics tags are speculative, but in my opinion justified - I think there's a good chance that, although this question isn't specifically about either topic, techniques from those topics may be relevant here. – Noah Schweber Jun 8 '19 at 7:10

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 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 $$ 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 http://www.mi-ras.ru/~bekl/Papers/ex2.ps . The argument above essentially is based on similar ideas, but for a simpler case.

 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.

• Thanks for the added detail - this is great! – Noah Schweber Jun 8 '19 at 8:54
• Out of curiosity, do you know of any other notation-independent definitions of proof-theoretic ordinals other than the sup of the ordertypes of primitive recursive relations the theory proves are well-founded? I remember hearing of such, but now that I think about it I can't recall any details. – Noah Schweber Jun 8 '19 at 8:55
• In the initial answer I claimed that my argument is essentially identical to the argument of Beklemishev, which isn't correct since Beklemishev actually proved stronger result. I have edited the answer accordingly. – Fedor Pakhomov Jun 8 '19 at 9:03
• Since that one requires a fixed system of fundamental sequences I think I still consider it notation-dependent. But it's definitely interesting! – Noah Schweber Jun 8 '19 at 9:14
• @NoahSchweber And there is a definition recently proposed by James Walsh and me ( arxiv.org/abs/1805.02095 ). Namely, one could consider the order on computably axiomatizable extensions $T$ of $\mathsf{ACA}_0$: $T_1<_{\Pi^1_1\text{-}RFN}T_2$ iff $T_2$ proves that $T_1$ is $\Pi^1_1$-sound. It happen that all $\Pi^1_1$-sound theories lie in the well-founded part of this order. Thus we have well-founded ranks for elements of this order. The correspondence with the standard proof-theoretic ordinals is that the theory with rank $\alpha$ have the proof-theoretic ordinal $\varepsilon_\alpha$. – Fedor Pakhomov Jun 8 '19 at 9:17