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.

  • 2
    $\begingroup$ 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. $\endgroup$ Oct 5, 2013 at 20:03
  • 3
    $\begingroup$ 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}$. $\endgroup$ Oct 5, 2013 at 20:04
  • $\begingroup$ 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. $\endgroup$ Oct 5, 2013 at 20:05
  • $\begingroup$ That's helpful, thank you both Noah and Andres. I will take a look at that Rathjen reference. $\endgroup$
    – user40919
    Oct 5, 2013 at 20:35

1 Answer 1


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."

  • 8
    $\begingroup$ Re: total lay-person-ness, let me clarify something: in the realm of proof-theoretic ordinals, I don't actually "know" anything. On the plus side, I have read a number of survey articles, and nodded my head sagely through dozens - dozens! - of conversations on the subject. :P $\endgroup$ Oct 5, 2013 at 20:54
  • 2
    $\begingroup$ 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.) $\endgroup$ Oct 5, 2013 at 20:56
  • 2
    $\begingroup$ 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." $\endgroup$ Oct 5, 2013 at 20:59
  • 2
    $\begingroup$ 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$. $\endgroup$ Oct 5, 2013 at 21:04
  • 2
    $\begingroup$ 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) $\endgroup$ Oct 5, 2013 at 21:12

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.