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

19more comments