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 ordinalof $T$ is the least ordinal $\alpha$ such that foreverynotation $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$?

techniquesfrom those topics may be relevant here. $\endgroup$ – Noah Schweber Jun 8 '19 at 7:10