Iterated Gentzen: or, a Sith objection to the proof of consistency of PA

Question

$\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$.

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}$.