How to understand the interface of the consistency strength hierarchy, reverse mathematics, and proof-theoretic ordinal analysis?

Question

I am aware of three major "hierarchies" of mathematical theories, but I don't know how to relate these hierarchies to one another. Here are the hierarchies I have in mind:

1. Consistency strength. My understanding is that here one considers (recursively-enumerable?) theories $T$ of arithmetic (or which interpret the language of first-order arithmetic) of sufficient strength to fix some scheme for the syntax of first-order languages. One (partially) orders these theories by saying that $T > T'$ if $T$ proves the consistency of $T'$ (when $T'$ is coded up according to the aforementioned syntactic scheme).

2. Reverse mathematics. My understanding is that here one considers theories $T$ of second-order arithmetic (or which interpret the language of second-order arithmetic) and (partially) orders them directly by their implications.

3. Proof-theoretic ordinal analysis. My understanding is that here one considers theories $T$ of arithmetic (or which interpret the language of first-order arithmetic) and orders them by their proof-theoretic ordinal, i.e. the supremum of all (countable) ordinals $\alpha$ such that there exists a relation $R \subseteq \mathbb N \times \mathbb N$ definable in $T$ such that $T$ proves that $R$ is a well-order (although the sense in which $T$ can even express that $R$ is a well-order if $T$ is first-order is something that I don't quite understand), and $R$ is (externally) isomorphic to $\alpha$.

Questions:

1. Where do the domains of applicability of these hierachies overlap?

For instance, it seems that the "strongest" theories (like ZFC+ large cardinals) are usually studied in terms of consistency strength as opposed to reverse math or proof theory. I have the impression that proof-theoretic ordinals are most commonly used for relatively weak theories, and that reverse math lies somewhere in the middle. But I'm not even sure where to look for the overlaps in these domains, partly because the sorts of theories considered in each hierarchy are slightly different.

2. Where there domains overlap, how do these hierarchies relate?

In general, I imagine there are no direct implications saying that any of these partial orders refines any of the others (even where their domains of applicability coincide). But I imagine that there are some general tendencies -- a stronger theory in one hierarchy should probably typically be stronger in another as well.

3. Should I really be thinking of these 3 hierarchies as "comparable" in the sense that they give some notion of "strength" of a theory? And are there other hierarchies I should have in mind in this regard as well?

Answer 1

Sorry this is a bit disjointed - there's a lot of stuff here. I hope this helps though.

---

All of these notions are applicable in all contexts - or at least, all sufficiently rich contexts (we probably want at least to interpret $PRA$). That said, once we get to reasonably strong theories (basically anything above $\Pi^1_2$-$CA_0$) we don't know how to calculate proof-theoretic ordinals, so in practice ordinal analysis doesn't reach (anywhere close to) ZFC-type theories.

Of course, ordinal analysis provides more than just a hierarchy - it assigns a "value" to each theory, independent of what other theories we're considering. The implication and consistency hierarchies don't do this, or at least not directly (see here for some pushback on this claim), so it's not surprising that calculating proof-theoretic ordinals is harder than comparing consistency strengths - although it may be surprising (it was to me) that it's that much harder.

---

At this point it's a good idea to get to defining proof-theoretic ordinals properly. There isn't a single definition here, and some definitions (most?) have an element of subjectivity (they require a preexisting notion of "natural ordinal notation"). My favorite definition - which is fully formal - is the following:

Set $PTO(T)$ to be the smallest $\alpha$ such that there is no (index for a) primitive recursive well-ordering isomorphic to $\alpha$ which $T$ proves is well-ordered.

This definition makes sense for theories in sufficiently rich languages (e.g. second-order arithmetic and set theory). This isn't too big an issue (e.g. $RCA_0$ is conservative over $I\Sigma_1$ and $ACA_0$ is conservative over $PA$), but we can whip up versions for first-order arithmetic by talking about provable induction schemes (e.g. "$T$ proves $\Sigma_1$-induction along (that notation for) $\alpha$"). Here we have another level of flexibility, namely how much induction along the notation we want; if I recall correctly at this point $\Sigma^0_1$ induction is the standard choice.

But there are many other kinds of proof-theoretic ordinal, and beyond this one notion I really have no relevant competency.

The key point is that we need to talk about only primitive recursive relations. For example, in $\Pi^1_1$-$CA_0$ we can define a canonical relation on $\omega$ of ("true") ordertype $\omega_1^{CK}$, and in $ZFC$ we can go galactically beyond that. The issue is that these aren't really "concrete," and if we're thinking of ordinal analysis as a tool for Gentzen-style consistency proofs we really want to work lower down.

• That said, we could look at very different ways of assigning ordinals to theories - see e.g. here.

---

Implication strength of course behaves quite differently from consistency strength/ordinal analysis. First, differences in language are a bit more significant here, and we have to talk about interpretations/conservative extensions. More importantly, while there are definitely large chunks of well-foundedness (for example: $I\Sigma_n/B\Sigma_n$; the Big Five (+ higher $\Pi^1_k$-$CA_0$s); $KP\omega+\Sigma_n$-Replacement; large chunks of the large cardinal hierarchy) there are important nonimplications amongst the natural theories (plenty in the context of choice fragments over $ZF$, and in reverse mathematics probably the most important - sociologically speaking - being $WKL_0\perp RT^2_2$).

That said, I know of relatively few situations where we have a strict inequality in consistency strength and no corresponding strict implication (or incompatibility: over ZFC, a measurable doesn't imply V=L but it does resolve it). Some occur in the large cardinal hierarchy, and by Montalban/Shore we know that the $n$-$\Pi^0_3$-determinacy hierarchy has lots of incomparabilities with the $\Pi^1_n$-$CA_0$ hierarchy, but it does seem to be pretty rare.

The three contexts mentioned - first-order arithmetic, second-order arithmetic, and set theory - do "glue together" reasonably well in terms of modified implication (= folding in appropriate interpretations to deal with language differences). E.g. $RCA_0$ is conservative over $I\Sigma_1$, and every model of $ATR_0$ is the set of reals of some model of $KP\omega$ (the converse fails though!). The real gulf comes in when we try to get from weak set theories (like $KP\omega$, $Z$, etc. - see here) to ZFC and its ilk. This gap is gigantic, and I know very little about it.

• As a trivial observation, implication strength is also much broader than consistency strength and ordinal analysis. The division between "classifying members/subclasses of a given class" and "comparing different axiom systems" is pretty subjective - there's no reason we couldn't think of either as the other.