9
$\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?

Improve this question
$\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$
    – Gabriel Nivasch
    Commented 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
    Commented Jan 5, 2020 at 20:22
  • 2
    $\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$
    – Timothy Chow
    Commented Jan 5, 2020 at 22:29
  • 1
    $\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
    Commented Jan 11, 2020 at 8:48

1 Answer 1

Reset to default
11
$\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.

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .