[proofplan] We argue by contradiction from a hypothetical $\mathrm{PA}$-proof of $0=1$. Gentzen's embedding translates this proof into a fixed sequent-calculus derivation, and Gentzen's ordinal assignment attaches to each derivation an ordinal notation below $\varepsilon_0$. The cut-reduction procedure strictly decreases this ordinal at every non-terminal stage, so the assumed transfinite induction schema below $\varepsilon_0$ forces termination in a cut-free derivation. This proof deliberately treats Gentzen's embedding theorem, ordinal-decrease theorem, and cut-free soundness theorem as cited metatheorems for the fixed calculus rather than reproving their proof-theoretic machinery. Finally, cut-free soundness in the standard model rules out a cut-free derivation of the contradictory sequent corresponding to $0=1$. [/proofplan] [step:Translate the assumed arithmetic contradiction into Gentzen sequent calculus] Assume, for contradiction, that $\mathrm{PA}$ is inconsistent. Then there exists a finite $\mathrm{PA}$-derivation $\pi$ whose final formula is $0=1$. Let $\mathsf{GPA}$ denote the fixed [Gentzen arithmetic sequent calculus](/page/Gentzen%20Arithmetic%20Sequent%20Calculus) presentation of first-order Peano arithmetic used in Gentzen's consistency proof: sequents are finite multisets $\Gamma \Rightarrow \Delta$ of first-order arithmetic formulas with equality; the logical rules are the classical structural, propositional, and quantifier rules specified in that calculus; equality is handled by its reflexivity and substitution initial sequents; and induction is represented by its Gentzen induction rule for arithmetic formulas. This linked definition fixes the exact proof system to which the ordinal assignment and reduction theorem below are attached. By the [Hilbert-to-Gentzen embedding theorem for Peano Arithmetic](/page/Hilbert-to-Gentzen%20Embedding%20for%20Peano%20Arithmetic) applied to this fixed $\mathsf{GPA}$, the proof $\pi$ determines a finite $\mathsf{GPA}$ derivation $\Pi$ of the succedent contradiction sequent corresponding to the theorem $0=1$, namely \begin{align*} \Rightarrow 0=1. \end{align*} The embedding theorem applies because each logical axiom, equality axiom, arithmetic axiom, modus ponens inference, quantifier inference, and induction instance of $\mathrm{PA}$ is simulated by finitely many rules or initial sequents of this same $\mathsf{GPA}$ presentation. Thus it is enough to show that no $\mathsf{GPA}$ derivation of $\Rightarrow 0=1$ exists. [guided] We begin with a proof in ordinary Peano Arithmetic and move to the proof system where Gentzen's reduction argument is formulated. The object $\pi$ is a finite syntactic derivation in $\mathrm{PA}$, and its final line is the closed formula $0=1$. Let $\mathsf{GPA}$ be the fixed Gentzen sequent calculus for arithmetic used throughout this proof. A sequent has the form $\Gamma \Rightarrow \Delta$, where $\Gamma$ and $\Delta$ are finite multisets of formulas in the first-order language of arithmetic with equality. The intended meaning is that the conjunction of the formulas in $\Gamma$ implies the disjunction of the formulas in $\Delta$. In this presentation, equality is governed by reflexivity and substitution initial sequents, and induction is governed by Gentzen's standard induction rule for arithmetic formulas. The formula $0=1$ as a theorem is represented by the succedent sequent \begin{align*} \Rightarrow 0=1. \end{align*} The [Hilbert-to-Gentzen embedding theorem for Peano Arithmetic](/page/Hilbert-to-Gentzen%20Embedding%20for%20Peano%20Arithmetic) says that every $\mathrm{PA}$ proof can be effectively transformed into a sequent derivation with the same final formula in this exact Gentzen arithmetic sequent calculus. The hypotheses of that embedding theorem match our setup: the language is the ordinary language of arithmetic with equality, the target calculus is the fixed $\mathsf{GPA}$ just defined, and that calculus contains the classical first-order rules, equality initial sequents, arithmetic initial sequents, and the Gentzen induction rule required by the theorem. Logical axioms become initial sequents or short logical derivations, modus ponens is simulated by cut, quantifier rules simulate the quantifier axioms, and induction instances are simulated by the induction rule. Therefore the assumed $\mathrm{PA}$ proof $\pi$ yields a finite $\mathsf{GPA}$ derivation $\Pi$ of $\Rightarrow 0=1$. [/guided] [/step] [step:Assign an ordinal below $\varepsilon_0$ to the sequent derivation] Let $\mathcal{O}_{<\varepsilon_0}$ denote Gentzen's fixed primitive recursive system of ordinal notations for ordinals below $\varepsilon_0$, and let $<_{\mathcal O}$ denote its primitive recursive strict ordering. The [Gentzen ordinal assignment below $\varepsilon_0$](/page/Gentzen%20Ordinal%20Assignment%20below%20Epsilon_0) for the fixed calculus $\mathsf{GPA}$ is a primitive recursive map \begin{align*} o:\{\text{finite }\mathsf{GPA}\text{-derivations}\} &\to \mathcal{O}_{<\varepsilon_0} \\ D &\mapsto o(D), \end{align*} with the property that $o(D)$ is a notation in $\mathcal{O}_{<\varepsilon_0}$ for every finite $\mathsf{GPA}$ derivation $D$. Apply this map to the derivation $\Pi$ and write \begin{align*} \alpha_0 := o(\Pi). \end{align*} Then $\alpha_0$ is an ordinal notation with $\alpha_0 < \varepsilon_0$. [guided] Gentzen's proof does not merely reduce proofs; it measures their complexity by ordinal notations. Let $\mathcal{O}_{<\varepsilon_0}$ be the fixed primitive recursive notation system for ordinals below $\varepsilon_0$, and let $<_{\mathcal O}$ be the primitive recursive strict ordering on those notations. The crucial syntactic construction for the same fixed calculus $\mathsf{GPA}$ is the [Gentzen ordinal assignment below $\varepsilon_0$](/page/Gentzen%20Ordinal%20Assignment%20below%20Epsilon_0), a primitive recursive map \begin{align*} o:\{\text{finite }\mathsf{GPA}\text{-derivations}\} &\to \mathcal{O}_{<\varepsilon_0} \\ D &\mapsto o(D). \end{align*} The value $o(D)$ records the height, cut ranks, and induction complexity of the derivation $D$ in a way calibrated to the ordinal $\varepsilon_0$. The point of using $\varepsilon_0$ is that the reductions needed for arithmetic may duplicate subderivations and therefore cannot be measured by a natural number alone, but their complexity is still bounded by ordinal notations below $\varepsilon_0$. For our particular contradiction derivation $\Pi$, define \begin{align*} \alpha_0 := o(\Pi). \end{align*} By construction of the ordinal assignment, $\alpha_0$ is a notation for an ordinal strictly below $\varepsilon_0$. [/guided] [/step] [step:Use Gentzen reductions to obtain a strictly descending ordinal sequence unless reduction terminates] Gentzen's reduction procedure is a primitive recursive partial map \begin{align*} R:\{\text{non-cut-free }\mathsf{GPA}\text{-derivations of }\Rightarrow 0=1\} &\to \{\mathsf{GPA}\text{-derivations of }\Rightarrow 0=1\} \\ D &\mapsto R(D), \end{align*} which transforms a non-cut-free derivation into another derivation of the same end-sequent. The [Gentzen ordinal-decrease theorem for reductions](/page/Gentzen%20Ordinal-Decrease%20Theorem%20for%20Reductions) applies to this exact $\mathsf{GPA}$ presentation, this exact ordinal assignment $o$, and this exact reduction map $R$. This theorem includes the verification that the reduction clauses for logical rules, cuts, equality, and the Gentzen induction rule preserve the end-sequent and strictly lower the assigned ordinal notation. It states that if $D$ is a finite non-cut-free $\mathsf{GPA}$ derivation of the end-sequent $\Rightarrow 0=1$, then $R(D)$ is a finite $\mathsf{GPA}$ derivation of the same end-sequent and \begin{align*} o(R(D)) <_{\mathcal O} o(D). \end{align*} Thus the theorem's hypotheses are satisfied whenever we apply $R$: the derivation is finite, belongs to the fixed Gentzen calculus with induction represented by its specified induction rule, has the fixed end-sequent $\Rightarrow 0=1$, and is not cut-free. Starting with $D_0 := \Pi$, define recursively, as long as possible, \begin{align*} D_{m+1} := R(D_m), \qquad \alpha_m := o(D_m). \end{align*} If the reduction process did not terminate, then $(\alpha_m)_{m\in\mathbb{N}}$ would be an infinite strictly descending sequence of ordinal notations below $\varepsilon_0$: \begin{align*} \alpha_{m+1} <_{\mathcal O} \alpha_m \end{align*} for every $m \in \mathbb{N}$. [guided] The reduction map $R$ is the operation that removes, lowers, or permutes cuts in a Gentzen derivation. Its domain consists of those derivations of the fixed end-sequent $\Rightarrow 0=1$ that are not yet cut-free. Formally, \begin{align*} R:\{\text{non-cut-free }\mathsf{GPA}\text{-derivations of }\Rightarrow 0=1\} &\to \{\mathsf{GPA}\text{-derivations of }\Rightarrow 0=1\} \\ D &\mapsto R(D). \end{align*} The important point is that $R$ preserves the final sequent. If $D$ proves $\Rightarrow 0=1$, then $R(D)$ also proves $\Rightarrow 0=1$. The reduction changes the proof, not the theorem proved. The main technical theorem behind Gentzen's argument is the [Gentzen ordinal-decrease theorem for reductions](/page/Gentzen%20Ordinal-Decrease%20Theorem%20for%20Reductions) for this exact setup. It requires a finite non-cut-free derivation in the fixed calculus $\mathsf{GPA}$, with induction represented by the specified Gentzen induction rule, and it uses the same ordinal assignment $o$ and the same reduction map $R$ defined above. The theorem's proof is where the difficult verification for reductions involving induction occurs; here it is used as a cited prerequisite. These hypotheses hold for each $D_m$ to which we apply $R$. The theorem concludes that \begin{align*} o(R(D_m)) <_{\mathcal O} o(D_m). \end{align*} This is the precise place where the ordinal assignment was engineered. Each local reduction either lowers the cut rank or moves a cut upward in a way that may duplicate proof material, and the ordinal measure below $\varepsilon_0$ is chosen so that the net effect is still a strict decrease in the notation ordering $<_{\mathcal O}$. Now define $D_0 := \Pi$. If $D_m$ is not cut-free, define \begin{align*} D_{m+1} := R(D_m). \end{align*} For every defined $D_m$, also define \begin{align*} \alpha_m := o(D_m). \end{align*} If this recursive construction never stopped, then the ordinal-decrease theorem would give \begin{align*} \alpha_{m+1} = o(D_{m+1}) = o(R(D_m)) <_{\mathcal O} o(D_m) = \alpha_m \end{align*} for every $m \in \mathbb{N}$. Thus a nonterminating reduction sequence would produce an infinite strictly descending sequence of ordinal notations below $\varepsilon_0$. [/guided] [/step] [step:Apply transfinite induction below $\varepsilon_0$ to force termination] By the theorem statement, the [transfinite induction schema below $\varepsilon_0$](/page/Transfinite%20Induction%20below%20Epsilon_0) is available for every arithmetical predicate on the fixed notation system $(\mathcal{O}_{<\varepsilon_0}, <_{\mathcal O})$. Apply this principle to the arithmetical predicate $P(\alpha)$ asserting that no reduction sequence starting from any derivation $D$ with $o(D)=\alpha$ is infinite. The predicate is arithmetical because finite derivations, the map $o$, the reduction map $R$, and the relation $<_{\mathcal O}$ are primitive recursive. The induction step follows from the strict decrease property: if every $\beta <_{\mathcal O} \alpha$ satisfies $P$, and $o(R(D)) <_{\mathcal O} o(D)=\alpha$, then the tail of the reduction sequence from $R(D)$ is finite, so the reduction sequence from $D$ is finite. Therefore the reduction process starting from $\Pi$ terminates. Hence there exists a cut-free $\mathsf{GPA}$ derivation $\Pi^\ast$ of the same end-sequent \begin{align*} \Rightarrow 0=1. \end{align*} [guided] The theorem assumes the [transfinite induction schema below $\varepsilon_0$](/page/Transfinite%20Induction%20below%20Epsilon_0), and this is exactly the principle needed to rule out the infinite descending ordinal sequence produced in the previous step. To make the use of induction explicit, define an arithmetical predicate $P$ on ordinal notations below $\varepsilon_0$ as follows: $P(\alpha)$ means that every Gentzen reduction sequence starting from every derivation $D$ with $o(D)=\alpha$ is finite. This predicate is arithmetical because derivations, reductions, and ordinal comparisons in the notation system are primitive recursive. We prove $P(\alpha)$ for all $\alpha \in \mathcal{O}_{<\varepsilon_0}$ by transfinite induction along $<_{\mathcal O}$. Fix $\alpha \in \mathcal{O}_{<\varepsilon_0}$ and assume as induction hypothesis that $P(\beta)$ holds for every $\beta <_{\mathcal O} \alpha$. Let $D$ be a derivation with $o(D)=\alpha$. If $D$ is already cut-free, then the reduction sequence from $D$ has length zero and is finite. If $D$ is not cut-free, then $R(D)$ is defined and the ordinal-decrease theorem gives \begin{align*} o(R(D)) <_{\mathcal O} o(D) = \alpha. \end{align*} By the induction hypothesis applied to $\beta := o(R(D))$, every reduction sequence starting from $R(D)$ is finite. Adding the single first reduction step $D \mapsto R(D)$ gives a finite reduction sequence starting from $D$. Thus $P(\alpha)$ holds for every $\alpha<\varepsilon_0$. In particular, it holds for $\alpha_0=o(\Pi)$. Therefore the reduction sequence starting from $\Pi$ terminates. Since the reduction map is defined exactly when a derivation is not cut-free, the terminal derivation $\Pi^\ast$ must be cut-free. Since each reduction preserves the end-sequent, $\Pi^\ast$ is a cut-free derivation of \begin{align*} \Rightarrow 0=1. \end{align*} [/guided] [/step] [step:Use cut-free soundness to rule out the terminal contradiction] We use the [cut-free soundness theorem for Gentzen arithmetic](/page/Cut-Free%20Soundness%20for%20Gentzen%20Arithmetic) for the fixed arithmetic sequent calculus $\mathsf{GPA}$: if a cut-free $\mathsf{GPA}$ derivation has end-sequent $\Gamma \Rightarrow \Delta$, then the standard model $\mathbb{N}$ satisfies that sequent under every variable assignment. This final step is a metamathematical semantic argument in the ordinary standard model; it is not presented here as a formalization inside a weak finitistic base theory. The theorem applies to this calculus because its initial sequents are true in $\mathbb{N}$, its equality initial sequents express reflexivity and substitutivity of equality in $\mathbb{N}$, its arithmetic initial sequents are true in $\mathbb{N}$, its induction rule is sound for subsets of $\mathbb{N}$ defined by arithmetic formulas, and each structural, propositional, and quantifier rule preserves truth of sequents. Apply this theorem to the cut-free derivation $\Pi^\ast$ of \begin{align*} \Rightarrow 0=1. \end{align*} The sequent has empty antecedent and the single closed succedent formula $0=1$, so its truth in $\mathbb{N}$ would mean that $\mathbb{N} \models 0=1$. But the interpretations of the numerals $0$ and $1$ in $\mathbb{N}$ are distinct natural numbers, so $\mathbb{N} \not\models 0=1$. Therefore no cut-free $\mathsf{GPA}$ derivation of $\Rightarrow 0=1$ exists, contradicting the existence of $\Pi^\ast$. [guided] The terminal derivation $\Pi^\ast$ is cut-free. Instead of relying on an informal inspection of the possible final rules, we use the precise [cut-free soundness theorem for Gentzen arithmetic](/page/Cut-Free%20Soundness%20for%20Gentzen%20Arithmetic) for the fixed calculus $\mathsf{GPA}$. The theorem says: if a cut-free $\mathsf{GPA}$ derivation ends in a sequent $\Gamma \Rightarrow \Delta$, then the standard model $\mathbb{N}$ satisfies that sequent under every assignment of values to its free variables. This is a semantic metatheoretic closure of the argument, not an internal finitistic formalization of the last step. We verify that the theorem applies to the proof system chosen earlier. Identity initial sequents $A \Rightarrow A$ are true in every structure. Equality initial sequents are true in $\mathbb{N}$ because equality on natural numbers is reflexive and substitutive for the interpretations of $0$, $S$, $+$, and $\cdot$. The arithmetic initial sequents are true in $\mathbb{N}$ by the intended interpretation of the symbols of arithmetic. The induction rule is sound because if an arithmetic formula holds at $0$ and is preserved from $n$ to $S(n)$ for every $n \in \mathbb{N}$, then ordinary induction in the standard model gives that it holds for every natural number. Finally, the structural, propositional, and quantifier rules preserve truth of sequents by the usual truth definitions for first-order logic. Now apply cut-free soundness to $\Pi^\ast$. Its end-sequent is \begin{align*} \Rightarrow 0=1. \end{align*} Since the antecedent is empty and the succedent contains only the closed formula $0=1$, the sequent is true in $\mathbb{N}$ exactly when $\mathbb{N} \models 0=1$. But $0$ and $1$ denote distinct natural numbers in the standard model, so \begin{align*} \mathbb{N} \not\models 0=1. \end{align*} Therefore the cut-free derivation $\Pi^\ast$ cannot exist. This contradicts the derivation obtained by the terminating Gentzen reduction process. [/guided] [/step] [step:Conclude that Peano Arithmetic is consistent] The contradiction arose from assuming that there exists a $\mathrm{PA}$ proof of $0=1$. Hence no such proof exists. Therefore $\mathrm{PA}$ is consistent. [/step]