$\DeclareMathOperator\PRA{PRA}\DeclareMathOperator\WF{WF}\DeclareMathOperator\Con{Con}\DeclareMathOperator\PA{PA}$Preamble: In the year … in a galaxy far far away, a nasty Sith named Darth Dubious (DD) asks a Jedi, Obi Wan Mathobi (OWM), about the consistency of PA:

DD: How do you know that PA is consistent?

OWM: Don't you know that many centuries ago a great Mathematician from Terra by the name of Gentzen proved its consistency?

DD: Of course I do. He proved that $\PRA + \WF(\epsilon_0) \vdash \Con(\PA)$, but ….

OWM: But what? Are you going to tell me the usual story that the proof is not finitistic enough?

DD: I dare not, Master Mathobi. I happily concede that the proof is valid. Yet, I have still a doubt lingering in my brain: how do you know that $G(0) =\PRA + \WF(\epsilon_0)$ itself is not contradictory?

As I said, the proof seems quite acceptable to me, but not any argument that $G(0)$ is consistent because it has a model in some very infinitistic theory such as ZF.

Rather, let us say that we apply Gentzen's argument to $G(0)$, and that we can prove the following: $\PRA + \WF(\alpha_0) \vdash \Con( G(0))$.

Now, I would surmise that $\alpha_0 > \epsilon_0$, right?

OWM: It would seem so. I suspect (but I am not sure) that else $\PA$ would be able to prove the consistency of $G(0)$. Need to ask some other Jedis more skillful in Ordinal Analysis ….

DD: Ok, waiting for them I tell you where I am going, although methinks you know it already: I am going to repeat my argument again, and create a chain of theories $G(i)$ such that each one Gentzen-proves the consistency of the previous one by an ever greater countable ordinal. If necessary, we can iterate beyond $\omega$. Now, is this series of countable recursive ordinals cofinal in the set of all countable recursive ordinals? If yes, I am afraid you ask for too much, because then I would have to accept induction all the way to $\omega^{CK}_1$.

If, on the other hand, it does not, I would like to know which is the upper bound.

THAT ordinal is the actual price to pay to secure $\PA$'s consistency.

Question: What is wrong with DD's argument? Or, if it is sound, any clues on the upper bound ordinal which would secure the consistency of the entire chain of iterated Gentzen theories

ADDENDUM I started with $\PA$ but, mutatis mutandis, you can begin from $\operatorname Q$, in which case instead of $\epsilon_0$ you use $\omega$.

  • 2
    $\begingroup$ There's a step "Now, I would surmise that $\alpha_0 > \epsilon_0$, right?" which is not fully justified, and seems to be the obvious place to look for trouble. $\endgroup$
    – LSpice
    Aug 15, 2020 at 18:44
  • 1
    $\begingroup$ LSpice, thanks for your editing. My eye sight is not that good, and I am quite sloppy. As for your point, of course, that is the "critical point", but we need details, don't we? Some Jedi Masters here know how to dig it, I trust.... $\endgroup$ Aug 15, 2020 at 18:46
  • 3
    $\begingroup$ If the argument already fails at step 0 then it has nowhere further to go, as $\operatorname{Con}(\epsilon_0) \vdash \operatorname{Con}(\alpha_0)$ in this case (right?). Anyway I am no logician, and agree that experts will chime in. I was just pointing out that there was an obvious point on which to focus. $\endgroup$
    – LSpice
    Aug 15, 2020 at 18:52
  • 2
    $\begingroup$ In order to really formalize this question, you may have to be more careful in terms of formalizing what you mean by $\mathrm{WF}(\alpha)$. $\mathrm{PRA}$ is a first-order theory of arithmetic, so right off the bat full well-foundedness is not formalizable. You can only talk about well-foundedness relative to descending sequences definable with formulas of some given complexity (and, indeed, Gentzen only needs it for some relatively low complexity). $\endgroup$ Aug 16, 2020 at 1:39
  • 2
    $\begingroup$ The other issue is that really you have to talk about specific ordinal notations (as in specific computable copies of the ordinals). Over a sufficiently strong base theory these different forms of the assumption should be provably equivalent, but I don't know if this true for arbitrarily large computable ordinals, and I don't know if it's true for $\mathrm{PRA}$. $\endgroup$ Aug 16, 2020 at 1:40

1 Answer 1


Mathobi is making a different argument in the comments on this post than in the question itself: in the post Mathobi is considering how far we need to justify transfinite induction to prove $G(i)$ consistent over PRA, while in the comments you mentioned Mathobi's hope would be supported if PA+Con(PA) had proof-theoretic ordinal $\varepsilon_0$. In favor of the position in the comments, the theories PA, PA+Con(PA), PA+Con(PA+Con(PA))), etc. (for finite iterations) all have the same strength, $\varepsilon_0$. However, we can show $G(1)$ is quite a bit stronger than PA+Con(PA), and each $G(i+1)$ is stronger than $G(i)$.

But first, we need to distinguish a few concepts: there's more than one formulation of proof-theoretic ordinal, the most commonly used one is $\vert\, .\,\vert_{sup}$, and $\vert\, .\,\vert_{Con}$ is the rendering of Gentzen's result in your question, $\textrm{PRA+TI}(\alpha)\vdash\textrm{Con(T)}$. (These are described in more detail in Rathjen's "The Realm of Ordinal Analysis".) However $\vert\, .\,\vert_{Con}$ is only useful with respect to a "natural" ordinal representation system fixed in advance, so for the rest of this answer we fix a representation system such as one based on Veblen's functions. Let's also define theories $H(0)=\textrm{PA}$, and $H(i+1)=\textrm{PA+Con}(H(i))$.

Here we get our first result comparing proof-theoretic ordinals of these theories, which is that for all $i<\omega$ we have $\vert H(i)\vert_{sup}=\varepsilon_0$. Since each $H(i)$ is a recursive theory, $\textrm{Con}(H(i))$ is a $\Pi_1^0$-sentence, and by proposition 2.24 from Rathjen's "The Realm of Ordinal Analysis", we have $\vert\textrm{PA+}\phi\vert_{sup}=\varepsilon_0$ where $\phi$ is any true arithmetical sentence. So we have $\vert\textrm{PA}\vert_{sup}=\vert \textrm{PA+Con}(H(i))\vert_{sup}$ for all $i<\omega$, and all those proof-theoretic ordinals are $\varepsilon_0$.

This doesn't fully answer the original question though, which was framed in terms of $\vert G(i)\vert_{Con}$ instead of $\vert H(i)\vert_{sup}$. The next step to answering the main question is utilizing this result to compare $\vert H(i)\vert_{Con}$, which also gives us that $\vert H(i)\vert_{Con}=\varepsilon_0$ for all $i<\omega$. (I can provide proof of this fact.)

However, failure to replicate this result for the hierarchy $G(i)$ shows the discrepancy between Mathobi's points: while for all $i<\omega$ we have $\vert H(i)\vert_{Con}=\vert H(i+1)\vert_{Con}$, in contrast we have $\vert G(i)\vert_{Con}<\vert G(i+1)\vert_{Con}$! (This is because otherwise $G(i+1)=\textrm{PRA+TI}(\vert G(i)\vert_{Con})=\textrm{PRA+TI}(\vert G(i+1)\vert_{Con})$ would prove its own consistency.) As a result $\textrm{PRA+TI}(\varepsilon_0)$ is quite a bit stronger than PA+Con(PA) at least in terms of $\vert\, .\,\vert_{Con}$.

  • $\begingroup$ C7X, you got my vote. A for a comment, give me some time to process your answer, and then I will add my reaction as an addendum to my post $\endgroup$ Apr 16, 2022 at 16:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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