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?

existenceof 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 Jan 5 at 22:29