# Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?

Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense the complexity or power of a theory.

Does anyone know what is the proof theoretic ordinal of $ZFC$ or any non-trivial $ZFC$ extensions? Wikipedia says this is unknown for $ZFC$ as of 2008, but maybe there has been some recent progress? Thank you.

• I believe that proof-theoretic ordinals for much weaker theories (e.g., $\Pi^1_3$-$CA_0$, a subtheory of second-order arithmetic) are still unknown; the state of the art appears to be around $\Pi^1_2$-$CA_0$, if I understand the state of things correctly. Oct 5, 2013 at 20:03
• No real progress towards this goal, in the sense that proof theory has a long way to go to reach $\mathsf{ZFC}$ or comparable theories. In some of his latest talks (on the consistency of $\mathsf{PA}$), Cohen suggested he had a way of understanding this ordinal $\alpha$, but I could never see a coherent presentation, and I doubt there was something sufficiently developed to allow us to unambiguously identify an ordinal as the proof-theoretic ordinal for $\mathsf{ZFC}$. Oct 5, 2013 at 20:04
• For example, already an analysis of $\Pi^1_2$-$CA_0$ by Rathjen required very complicated ordinal notations, and recently (see the intro to miami.uni-muenster.de/servlets/DerivateServlet/Derivate-5965/…) a serious error was found (and patched, I think) in Rathjen's work around this level. Oct 5, 2013 at 20:05
• That's helpful, thank you both Noah and Andres. I will take a look at that Rathjen reference. Oct 5, 2013 at 20:35

As Andres and I have stated in the comments, we are still nowhere near a proof-theoretic analysis of $ZFC$ or similar theories; even full second-order arithmetic remains well out of reach.
The paper "The Art of Ordinal Analysis" by Michael Rathjen does a good job of both describing ordinal analyses which have succeeded (e.g., $PA$), and showing how new difficulties arise as we climb towards higher and higher comprehension axioms (still around the level of $\Pi^1_2$-$CA_0$ by the end of the paper). I think this might be worth reading, if you want an explanation of why finding proof-theoretic ordinals of strong theories is "hard."
• First of all, since $SOA$ is a subtheory of $ZFC$, all the difficulties of analyzing $SOA$ will surely show up in trying to analyze $ZFC$; so at the very least, $SOA$ should be far easier to understand than $ZFC$. (In particular, I expect $SOA$ to be analyzed in my lifetime; I do not expect that of $ZFC$, and in fact would be very surprised if I lived to see it.) Oct 5, 2013 at 20:56
• Second, $SOA$ and $ZFC$ aren't really that alien; already in analyzing subtheories of $SOA$, it has been extremely useful to recast them as weak set theories, such as $KP$; see section 2.2 of Rathjen's paper. So in analyzing bigger and bigger subsystems of $SOA$, we're already "climbing towards" $ZFC$ in some sense; it seems reasonable that this will be how we eventually get to $ZFC$. So then not only is $SOA$ likely easier than $ZFC$, it is probably an actual "step along the way." Oct 5, 2013 at 20:59
• Finally, the techniques used in ordinal analyses have been revolutionized multiple times already in the course of getting to (somewhere around) $\Pi^1_2$-$CA_0$. The twist that is dearest to my heart is the use of uncountable cardinals in ordinal notations developed by Bachmann (mentioned by Rathjen on pp. 11), but Rathjen's article describes a number of interesting developments. The point is, "ordinal analysis" is not one specific tool that could reach $ZFC$ if we just put more effort into it; rather, it has needed many fundamentally new ways of thinking even to get up to $\Pi^1_2$-$CA_0$. Oct 5, 2013 at 21:04
• What does this mean? Well, ultimately, in coming up with these new approaches to ordinal analysis, I think one of the key things we'll need is good guesses about what might work. Trying to find the proof-theoretic ordinal of $ZFC$, there is simply too much we don't know how to do: I don't think spinning one's wheels trying to study $ZFC$ directly will pay off. By contrast, $SOA$ is far out of reach, but close enough that studying it right now (or soon) might actually pay off. We'll need the tools we develop in analyzing $SOA$ to analyze $ZFC$, anyways; and it might be much easier (cont'd) Oct 5, 2013 at 21:12