4
$\begingroup$

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

$\endgroup$
22
  • 1
    $\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 '20 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$ – Mirco A. Mannucci Aug 15 '20 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 '20 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$ – James Hanson Aug 16 '20 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$ – James Hanson Aug 16 '20 at 1:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.