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}$](https://en.wikipedia.org/wiki/Kleene%27s_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](https://mathoverflow.net/a/333516/8133), 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$?



Proof-theoretic ordinals: inevitable consistency?
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]](https://www.mi-ras.ru/%7Ebekl/Papers/ex2.ps). 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.


