4
$\begingroup$

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$?
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Noah Schweber Jun 8 '19 at 7:10
5
$\begingroup$

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 http://www.mi-ras.ru/~bekl/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.

$\endgroup$
  • $\begingroup$ Thanks for the added detail - this is great! $\endgroup$ – Noah Schweber Jun 8 '19 at 8:54
  • $\begingroup$ 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. $\endgroup$ – Noah Schweber Jun 8 '19 at 8:55
  • $\begingroup$ 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. $\endgroup$ – Fedor Pakhomov Jun 8 '19 at 9:03
  • 1
    $\begingroup$ Since that one requires a fixed system of fundamental sequences I think I still consider it notation-dependent. But it's definitely interesting! $\endgroup$ – Noah Schweber Jun 8 '19 at 9:14
  • 2
    $\begingroup$ @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$. $\endgroup$ – Fedor Pakhomov Jun 8 '19 at 9:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.