# Gentzen's result on PA

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?

• 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 Jan 5 '20 at 19:47
• 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. Jan 5 '20 at 20:22
• 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. Jan 5 '20 at 22:29
• 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
– none
Jan 11 '20 at 8:48

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.
• What's a reference for the claim that things can be improved to a $\Sigma_1$ or $\Delta_0$ formula? Jan 6 '20 at 11:41