Ordinal analysis and proofs of consistency

Question

$\epsilon_0$ is the proof-theoretic ordinal of PA. Gentzen proved the consistency of Peano's first-order axioms for arithmetic using primitive recursive arithmetic and induction up to $\epsilon_0$.

For what other interesting theories $T$ can induction up to the proof-theoretic ordinal of $T$, together with some weak principles such as primitive recursive arithmetic, prove the consistency of $T$?

For example: is there a recursive ordinal $\alpha$ such that induction up to $\alpha$, together with primitive recursive arithmetic, can prove the consistency of ZF?

Answer 1

In the field of ordinal analysis people are typically interested in finding "natural" computable ordinal notation systems corresponding to various theories; those are called proof-theoretic ordinals of the theories. Unfortunately we don't have any formal definition of "naturality" of ordinal notation systems, those is notion is vague.

Nevertheless there is the following empirical fact about what a calculation of proof-theoretic ordinal $|T|$ for natural systems $T$ give:

• theory $\mathsf{PRA}+\text{transfinite induction up to }|T|$ proves consistency of $T$;
• if the language of $T$ could express the sentences $\mathsf{WO}(R)$ "a primitive-recursive binary relation $R$ is a well-order" then $\sup \{|R|\mid T\vdash \mathsf{WO}(R)\}=|T|$;
• theory $T$ proves totalitly of all computable functions $H_{\alpha}(x)$, for $\alpha<|T|$, but doesn't prove totality of the computable function $H_{|T|}(x)$, where Hardy hierarchy $H_{\alpha}(x)$ is defined by transfinite recurtion for $\alpha\le|T|$: $$H_0(x)=x+1,\;\;\;H_{\alpha+1}(x)=H_{\alpha}(x+1)\;\;\;H_{\lambda}(x)=H_{\lambda[x]}(x),$$ here we presume that for limit $\lambda\le |T|$ we have fixed fundamental sequences $\lambda[0]<\lambda[1]<\ldots$ such that $\sup_{i\in \omega}\lambda[i]=\lambda$.

Some relatively well-known systems and their proof-theoretic ordinals in the order of strength increase

• $|\mathsf{PA}|=|\mathsf{ACA}_0|=\varepsilon_0$
• $|\mathsf{ATR}_0|=\Gamma_0$
• $|\mathsf{KP}\omega|=|\mathsf{ID}_1|=|\textsf{parameter free }\Pi^1_1\text{-}CA_0|=\psi_0(\varepsilon_{\Omega+1})$
• $|\Pi^1_1\text{-}CA_0|=\psi_0(\Omega_{\omega})$

Note that the ordinals ordinals for the last two group are from ordinal notation systems defined by people doing ordinal analysis. And hence would be hardly familiar to the people that aren't really familiar with the field.

The strength of the theories for which we do now know proof-theoretic ordinals are fairly limited. Namely the strongest systems for which a computation of proof-theoretic ordinal have been published (by M.Rathjen) is the (fairly strong) fragment of second-order arithmetic $\text{parameter free }\Pi^1_2\text{-}CA_0+\mathsf{BI}$. It is stronger than $\Pi^1_1\text{-}CA_0$, e.g. the strongest fragment in Simpson's big five of systems typically appearing in the context of reverse math. But the calculations of ordinals of $\mathsf{ZFC}$ and full second-order arithmetic arithmetic are beyond the reach of current methods.

However if one isn't interested in "naturality" of computable ordinal notation systems. Then it is fairly trivial to craft computable ordinal notation system corresponding to any given $\Pi^1_1$-sound theory $T$. Namely the idea is to craft computable linear ordering with the order type $$\sum\limits_{T\vdash\mathsf{WO}(R_i)} R_i,$$ where $R_0,R_1,\ldots$ is an enumeration of primitive-recursive binary relations.

For more details you could look at some surveys of the subject. For example

[1]Rathjen, M. (2006, August). The art of ordinal analysis. In Proceedings of the International Congress of Mathematicians (Vol. 2, pp. 45-69).

Answer 2

This depends on how you define "proof-theoretic ordinal." I would say that to seriously address this question we need to restrict attention to a fully-objective definition (as opposed to one dependent on choice of notation; the answer then is that the proof-theoretic ordinal of an appropriate (= "does enough arithmetic") theory always exists, and all existing evidence points to it having the desired consistency-proving property (and so we expect the same to hold for ZF), but there is (to my knowledge) no metatheorem establishing that this in fact holds.

In terms of how far ordinal analysis has been carried out in a way considered satisfying by the community (see the subtleties below), I believe the state-of-the-art is around $\Pi^1_2$-CA$_0$. My understanding is that ATR$_0$ represents the upper limit of the "relatively simple" analyses, and after that things get quite weird. But I'm not an expert.

Related:

• This paper by Rathjen is a good survey of general ordinal analysis.

• I vaguely remember an excellent paper (by Avigad?) summarizing different definitions of proof-theoretic ordinal and analyzing their relationships; if I can find it, I'll add it.

• This paper by Arai (and its sequel) isn't directly relevant, but looks at a different way to analyze (set) theories in terms of ordinals - focusing not on establishing consistency but on determining how complicated constructions the theory can establish. This approach is sufficiently "coarse" that it is quite feasible even at the level of ZF.

CAVEAT: Below I'm being a bit vague about what "proves induction along" means. In a theory in second-order arithmetic we can talk directly about well-orderedness; in a first-order theory we need to talk instead about fragments of induction (e.g. $\Sigma_1$-induction along the ordering in question).

---

A snappy definition you'll often see is indeed "The smallest ordinal such that induction along that ordinal proves (over PRA) the consistency of $T$." Of course this isn't really precise. Rather, we need to talk about ordinal notations: ignoring the details, these are just primitive recursive well-orderings of $\omega$ (ignoring the finite ones for now). Note that the set of actual notations is $\Pi^1_1$-complete.

The problem is that notations can be quite pathological. Consider for example the following way to build a linear order $\triangleleft$: we lay down points in order $$0\triangleleft 1\triangleleft 2\triangleleft ...$$ until we see a proof of $\perp$ in $T$, at which point we switch to building a copy of the "reversed" natural numbers. E.g. if the shortest proof of $\perp$ in $T$ has length $17$, we wind up building $$... 19\triangleleft 18\triangleleft 17\triangleleft 0\triangleleft 1\triangleleft 2\triangleleft 3\triangleleft ...\triangleleft 16.$$ There is a notation capturing this construction, and trivially induction along this notation proves (over PRA) the consistency of $T$. But its ordertype is just $\omega$ - did we just prove that every (appropriate) theory has proof-theoretic ordinal $\omega$?

No - when we say "induction along $\alpha$ proves the consistency of $T$," what we really mean is that there is some natural system of unique notations for ordinals up to $\alpha+1$ such that induction along the notation for $\alpha$ in this system proves (over PRA) the consistency of $T$, but induction along any smaller notation doesn't.

Of course this is a fundamentally vague task. In general though three other phenomena help motivate the specific choice:

• The systems so produced tend to "cohere" - e.g. there's a "simple" translation according to which the system for ATR$_0$ extends the system for PA.

• $T$ itself tends to (indeed, in every case I'm aware of does) prove induction along each smaller notation in that system.

• The system itself emerges naturally from an analysis of proofs from $T$ (e.g. by looking at cut elimination processes).

---

By contrast, a fully notation-independent definition is the following:

The computational proof-theoretic ordinal $\vert T\vert_{comp}$ of $T$ is the supremum of the computable ordinals $\alpha$ such that there is some notation $n$ for $\alpha$ which $T$ proves is well-founded.

This makes sense for any (appropriate) theory $T$, and - so long as $T$ is sufficiently sound - is always striclty less than $\omega_1^{CK}$ (by $\Sigma^1_1$ bounding). It turns out that we have the following phenomenon:

For every "natural" theory $T$, there is a "natural" notation for $\vert T\vert_{comp}$ such that induction along that notation proves (over PRA) the consistency of $T$.

But as far as I know there is no meta-theorem which says that this will always be the case, and indeed I don't even know what such a theory would look like (you'd have to somehow pin down what a "reasonable" ordinal notation is). So while (as far as I know) this phenomenon is expected to hold for all natural theories, and in particular for ZF, that is open.

---

Another reasonable attempt at a "notation-independent" definition would be the following:

The inevitable proof-theoretic ordinal $\vert T\vert_{inev}$ is the least computable ordinal $\alpha$ such that for every notation $n$ for $\alpha$, induction along $n$ proves (over PRA) the consistency of $T$.

But it's not clear to me that such a thing exists in general. Indeed, even for PA I'm not sure if such a thing exists, let alone that it is $\epsilon_0$: why shouldn't there be useless notations for long ordinals?

EDIT: Fedor Pakhomov pointed out below that Beklemishev showed that this never exists.