8
$\begingroup$

The Wikipedia states that Gentzen proved that "in modern terms, the proof-theoretic ordinal of PA is $\varepsilon_0$." Further down, the article defines what the "proof theoretic ordinal" of a theory means. However, I'm not sure what this means regarding PA, since PA can only make finitary statements.

Let me elaborate. Define some encoding of the ordinals ${}<\varepsilon_0$ as natural numbers. This encoding allows us to express statements involving ordinals ${}<\varepsilon_0$ in PA. Then, allegedly PA cannot prove transfinite induction using this encoding.

But what does this mean exactly? One option would be using sets: "Suppose $S$ is a set of ordinals such that, for every $\beta<\varepsilon_0$, whenever $\alpha\in S$ for every $\alpha<\beta$, we also have $\beta\in S$. Then $\beta\in S$ for all $\beta<\varepsilon_0$."

But this is an infinitary statement, as far as I understand, so it cannot be stated in PA.

Another option is to have a schema of infinitely many statements, one for each possible formula $\varphi$ (just like the "induction schema" contains infinitely many axioms, one for each possible formula):

"Suppose that for every $\beta<\varepsilon_0$, whenever $\varphi(\alpha)$ holds for every $\alpha<\beta$, we also have $\varphi(\beta)$. Then $\varphi(\beta)$ holds for every $\beta<\varepsilon_0$."

So what is it exactly that Gentzen proved? Presumably PA can prove the above statement for some formulas $\varphi$. So did Gentzen find some specific $\varphi$ for which PA cannot prove the above statement? Or what?

$\endgroup$
4
  • $\begingroup$ I saw question mathoverflow.net/questions/5065 , and it does not answer my question. Over there, the OP wanted to know how you encode ordinals <eps_0 as natural numbers. I understand how you do that $\endgroup$ Jan 5, 2020 at 19:47
  • 1
    $\begingroup$ To answer the first part of the question: yes, transfinite induction is stated as a schema, just like usual induction. When talking about theories weaker than PA we may want to restrict which formulas we include (e.g. only quantifier-free or bounded ones), but for PA and stronger it doesn't matter. $\endgroup$
    – Wojowu
    Jan 5, 2020 at 20:22
  • 1
    $\begingroup$ Noah Schweber has answered your question, but note that the existence of some $\varphi$ follows from Gentzen's consistency proof. Namely, if there were no such $\varphi$, then by mimicking Gentzen's consistency proof, we would be able to prove the consistency of PA within PA itself. $\endgroup$ Jan 5, 2020 at 22:29
  • $\begingroup$ I found an online draft of this book (Proof theory, by Herman Ruge Jervell) to be a very accessible introduction to Gentzen's proof and the concepts leading up to it. The draft is no longer at its old location but $\endgroup$
    – none
    Jan 11, 2020 at 8:48

1 Answer 1

10
$\begingroup$

Yes, Gentzen found a single "induction instance" which is PA-unprovable: more-or-less $\varphi(\alpha)$ = "Every sentence with a proof of cut-rank $\alpha$ has a cut-free proof."

Now, this $\varphi$ is a $\Pi^0_2$ formula. If memory serves, this is suboptimal: with some coding work this can be improved from a $\Pi^0_2$ formula to a $\Sigma^0_1$ formula. The basic idea is to assign in a primitive recursive way to each ordinal $\alpha<\epsilon_0$ a sentence $p_\alpha$ and a candidate proof $s_\alpha$ of cut rank $<\alpha$ such that each pair occurs cofinally often, and then look at the formula $\psi(\alpha)$ = "Either $s_\alpha$ is not a proof of $p_\alpha$ or there is a cut free proof of $p_\alpha$."

And I think even that's suboptimal - that we can get to the level of $\Delta_0$ - but I'm not sure.

$\endgroup$
1
  • 2
    $\begingroup$ What's a reference for the claim that things can be improved to a $\Sigma_1$ or $\Delta_0$ formula? $\endgroup$ Jan 6, 2020 at 11:41

Your Answer

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

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