[proofplan]
This proof records the standard corollary of Gentzen's ordinal analysis rather than reconstructing the full cut-reduction argument. The external metamathematical inputs are stated in the precise forms needed: Gentzen's fixed-instance theorem gives, for each externally fixed notation below $\varepsilon_0$, a finite $\mathrm{PA}$-proof of the corresponding transfinite-induction sentence, and Gentzen's formalized reduction theorem gives a single arithmetical predicate whose uniform induction instance implies $\operatorname{Con}(\mathrm{PA})$ over $\mathrm{PA}$. [Gödel's Second Incompleteness Theorem](/theorems/1508) then rules out $\mathrm{PA}$ proving all instances of that uniform scheme, assuming $\mathrm{PA}$ is consistent. Finally, we identify this fixed-instance plus uniform-unprovability characterization with the usual supremum definition of the proof-theoretic ordinal of $\mathrm{PA}$.
[/proofplan]
[step:Name the formal theories and the uniform induction scheme]
Let $\mathrm{PA}$ denote first-order Peano Arithmetic in the usual language of arithmetic. Let $\mathcal O_{<\varepsilon_0} \subseteq \mathbb N$ be the fixed primitive recursive notation system from the theorem statement, let $O(a)$ be the primitive recursive arithmetical formula expressing $a \in \mathcal O_{<\varepsilon_0}$, and let $<_\mathcal O$ denote its primitive recursive ordering relation. For a notation $a \in \mathcal O_{<\varepsilon_0}$ and an arithmetical formula $P(x)$ with one free variable, define the arithmetical sentence $\operatorname{TI}(a,P)$ by
\begin{align*}
\left(\forall b\,\left(b <_\mathcal O a \implies \left(\forall c\,\left(c <_\mathcal O b \implies P(c)\right) \implies P(b)\right)\right)\right)
\implies
\forall b\,\left(b <_\mathcal O a \implies P(b)\right).
\end{align*}
For each arithmetical formula $P(x)$, define the corresponding uniform sentence $\operatorname{UTI}_{<\varepsilon_0}(P)$ by
\begin{align*}
\forall a\,\left(O(a) \implies \operatorname{TI}(a,P)\right).
\end{align*}
The uniform transfinite-induction scheme $\operatorname{UTI}_{<\varepsilon_0}$ is the metatheoretic collection of all sentences $\operatorname{UTI}_{<\varepsilon_0}(P)$ as $P(x)$ ranges over arithmetical formulas. Thus the expression "$\mathrm{PA}$ proves $\operatorname{UTI}_{<\varepsilon_0}$" means that $\mathrm{PA}$ proves every sentence in this recursive scheme, not that there is a first-order quantifier over formulas inside $\mathrm{PA}$.
[/step]
[step:Apply Gentzen's fixed-instance theorem below $\varepsilon_0$]
We use the fixed-instance form of Gentzen's ordinal analysis: for the standard primitive recursive notation system $\mathcal O_{<\varepsilon_0}$, every externally fixed notation $a \in \mathcal O_{<\varepsilon_0}$ and every arithmetical formula $P(x)$ determine a finite $\mathrm{PA}$-proof of the sentence $\operatorname{TI}(a,P)$. This is not the uniform assertion that $\mathrm{PA}$ proves $\operatorname{UTI}_{<\varepsilon_0}(P)$; the notation $a$ is fixed in the metatheory before the proof is constructed. The hypotheses of the fixed-instance theorem match the present setting because $\mathcal O_{<\varepsilon_0}$ is the standard primitive recursive notation system fixed in the theorem statement, $a$ is fixed externally, and $P(x)$ is arithmetical. Therefore, for every fixed $\alpha \in \mathcal O_{<\varepsilon_0}$ and every arithmetical formula $P(x)$,
\begin{align*}
\mathrm{PA} \vdash \operatorname{TI}(\alpha,P).
\end{align*}
[guided]
The first half of the theorem is a fixed-instance assertion, not the uniform induction scheme. The fixed-instance form of Gentzen's ordinal analysis says the following precise metatheoretic statement: given a particular code $a$ for an ordinal notation below $\varepsilon_0$ and a particular arithmetical formula $P(x)$, Gentzen's reduction construction yields a finite derivation in $\mathrm{PA}$ of the sentence $\operatorname{TI}(a,P)$.
We verify that this external theorem applies. The notation system required by the theorem is the standard primitive recursive system below $\varepsilon_0$, and this is exactly the system $\mathcal O_{<\varepsilon_0}$ fixed in the statement. The input notation is not a variable ranging over all notations inside $\mathrm{PA}$; it is the chosen external notation $a=\alpha$. The predicate being inducted over is supplied by the arithmetical formula $P(x)$. Hence the fixed-instance theorem gives
\begin{align*}
\mathrm{PA} \vdash \operatorname{TI}(\alpha,P).
\end{align*}
This proves precisely the fixed-initial-segment assertion and does not assume the uniform scheme that will later be shown unprovable.
[/guided]
[/step]
[step:Extract the single uniform instance needed for Gentzen consistency]
Let $\operatorname{Prf}_{\mathrm{PA}}(n,m)$ be the standard primitive recursive proof predicate expressing that $n$ codes a $\mathrm{PA}$-proof of the formula with Gödel number $m$. Let $\bot$ denote the Gödel number of a fixed contradiction, and define the standard Hilbert-Bernays consistency sentence
\begin{align*}
\operatorname{Con}(\mathrm{PA}) := \forall n\,\neg \operatorname{Prf}_{\mathrm{PA}}(n,\bot).
\end{align*}
We use the formalized Gentzen reduction theorem in the following precise form: there is a fixed arithmetical formula $G(x)$ such that
\begin{align*}
\mathrm{PA} \vdash \operatorname{UTI}_{<\varepsilon_0}(G) \implies \operatorname{Con}(\mathrm{PA}).
\end{align*}
Here $G(x)$ is the primitive-recursive reduction invariant saying, in arithmetized form, that no reduction sequence starting from a derivation assigned an ordinal notation below $x$ reaches a contradiction. The theorem applies because $\operatorname{Prf}_{\mathrm{PA}}$ is primitive recursive, the ordinal assignment to finite $\mathrm{PA}$-derivations is primitive recursive, and the Gentzen reduction relation is primitive recursive and strictly decreases the assigned notation with respect to $<_\mathcal O$.
[guided]
The scheme $\operatorname{UTI}_{<\varepsilon_0}$ is not itself one formula of arithmetic, so the consistency argument must use a particular instance of the scheme. Gentzen's formalized reduction theorem supplies exactly such an instance. It constructs a fixed arithmetical formula $G(x)$ expressing the reduction invariant for derivations whose assigned ordinal notation is below $x$.
We define the consistency sentence carefully. The predicate $\operatorname{Prf}_{\mathrm{PA}}(n,m)$ is the standard primitive recursive relation saying that $n$ is the code of a $\mathrm{PA}$-proof of the formula with Gödel number $m$. If $\bot$ is the Gödel number of a fixed contradiction, then
\begin{align*}
\operatorname{Con}(\mathrm{PA}) := \forall n\,\neg \operatorname{Prf}_{\mathrm{PA}}(n,\bot)
\end{align*}
is the usual arithmetized consistency statement for $\mathrm{PA}$.
The formalized Gentzen reduction theorem verifies, inside $\mathrm{PA}$, that the ordinal assignment to derivations and the reduction relation are primitive recursive and that each reduction step strictly decreases the assigned notation in $<_\mathcal O$. Uniform transfinite induction for the single formula $G(x)$ rules out an infinite descending reduction sequence below $\varepsilon_0$. Therefore a derivation of contradiction cannot exist, and the theorem yields the internal implication
\begin{align*}
\mathrm{PA} \vdash \operatorname{UTI}_{<\varepsilon_0}(G) \implies \operatorname{Con}(\mathrm{PA}).
\end{align*}
This is the precise sense in which the uniform scheme is used: only one arithmetical instance $\operatorname{UTI}_{<\varepsilon_0}(G)$ is needed to derive consistency.
[/guided]
[/step]
[step:Use Gödel's Second Incompleteness Theorem to rule out PA proofs of all uniform instances]
Assume $\mathrm{PA}$ is consistent. Gödel's Second Incompleteness Theorem applies to $\mathrm{PA}$ with the Hilbert-Bernays consistency sentence $\operatorname{Con}(\mathrm{PA})$ defined above, because $\mathrm{PA}$ is recursively axiomatized, represents primitive recursive proof predicates, and satisfies the standard derivability conditions for its provability predicate. Hence
\begin{align*}
\mathrm{PA} \nvdash \operatorname{Con}(\mathrm{PA}).
\end{align*}
If $\mathrm{PA}$ proved every instance of the scheme $\operatorname{UTI}_{<\varepsilon_0}$, then in particular it would prove the Gentzen instance $\operatorname{UTI}_{<\varepsilon_0}(G)$. Combining that proof with
\begin{align*}
\mathrm{PA} \vdash \operatorname{UTI}_{<\varepsilon_0}(G) \implies \operatorname{Con}(\mathrm{PA})
\end{align*}
would give a $\mathrm{PA}$-proof of $\operatorname{Con}(\mathrm{PA})$ by modus ponens, contradicting Gödel's theorem. Therefore, assuming $\mathrm{PA}$ is consistent, $\mathrm{PA}$ does not prove every instance of $\operatorname{UTI}_{<\varepsilon_0}$.
[guided]
We now convert the consistency implication into an unprovability result. Gödel's Second Incompleteness Theorem applies specifically to the Hilbert-Bernays consistency sentence
\begin{align*}
\operatorname{Con}(\mathrm{PA}) := \forall n\,\neg \operatorname{Prf}_{\mathrm{PA}}(n,\bot),
\end{align*}
where $\operatorname{Prf}_{\mathrm{PA}}$ is the standard primitive recursive proof predicate. The theorem applies because $\mathrm{PA}$ is recursively axiomatized, contains enough arithmetic to represent primitive recursive relations, and its standard provability predicate satisfies the Hilbert-Bernays derivability conditions. Under the assumption that $\mathrm{PA}$ is consistent, Gödel's theorem gives
\begin{align*}
\mathrm{PA} \nvdash \operatorname{Con}(\mathrm{PA}).
\end{align*}
Suppose, toward a contradiction, that $\mathrm{PA}$ proved every sentence in the scheme $\operatorname{UTI}_{<\varepsilon_0}$. Then $\mathrm{PA}$ would prove the particular sentence $\operatorname{UTI}_{<\varepsilon_0}(G)$ from the previous step. The formalized Gentzen reduction theorem gives
\begin{align*}
\mathrm{PA} \vdash \operatorname{UTI}_{<\varepsilon_0}(G) \implies \operatorname{Con}(\mathrm{PA}).
\end{align*}
Applying modus ponens to these two $\mathrm{PA}$-proofs would produce
\begin{align*}
\mathrm{PA} \vdash \operatorname{Con}(\mathrm{PA}),
\end{align*}
which contradicts Gödel's Second Incompleteness Theorem. Hence $\mathrm{PA}$ cannot prove all instances of the uniform transfinite-induction scheme below $\varepsilon_0$.
[/guided]
[/step]
[step:Identify the resulting proof-theoretic ordinal]
We use the standard ordinal-analysis definition: the proof-theoretic ordinal of a recursively axiomatized arithmetical theory $T$ is the supremum of the ordinals represented by primitive recursive notation systems whose well-foundedness, equivalently the corresponding arithmetical transfinite-induction instances, are provable in $T$. Gentzen's fixed-instance theorem gives the lower-bound direction for $\mathrm{PA}$: every notation $\alpha \in \mathcal O_{<\varepsilon_0}$ has its fixed transfinite-induction instances provable in $\mathrm{PA}$, so all ordinals below $\varepsilon_0$ are reached.
The formalized Gentzen reduction theorem and Gödel's Second Incompleteness Theorem give the matching upper-bound obstruction. If $\mathrm{PA}$ proved the full uniform well-foundedness scheme for the standard system $\mathcal O_{<\varepsilon_0}$, then it would prove $\operatorname{Con}(\mathrm{PA})$, contradicting Gödel's theorem under the consistency assumption. The usual equivalence theorem for primitive recursive ordinal notation systems identifies this obstruction with the statement that no provably well-founded primitive recursive ordinal notation system for $\mathrm{PA}$ has order type reaching or exceeding $\varepsilon_0$. Hence the supremum is exactly $\varepsilon_0$, which is the asserted proof-theoretic ordinal of Peano Arithmetic.
[/step]
