The Wikipedia [states](https://en.wikipedia.org/wiki/Ordinal_analysis) 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?



Gentzen's result on PA
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.


