If PA were inconsistent, there would exist a proof P of the empty sequent, and the sequence g(0) > g(1) > g(2) > ... would be an infinite strictly descending sequence of ordinals below epsilon_0.
First-order Peano arithmetic, a formal axiom system that approximates the mathematical axioms employed in practice
Strictly descending sequence(describing the pattern of the sequence g(0) > g(1) > g(2))
A list of values that gets smaller and smaller with each step, where nothing can ever stay the same or increase—each value must be strictly less than the one before.
empty sequent
A sequent with no formulas on either side, representing a proof of contradiction (inconsistency) in the sequent calculus
ordinals(Proof-theoretic treatment of ordinals, distinct from but related to set-theoretic ordinals)
A central concept in both set theory and proof theory, used by Gentzen to assign measures to proofs in order to demonstrate consistency of PA via well-foundedness
proof(Frege's formal system; the definition still used by logicians today)
Any finite sequence of statements such that each statement is either an axiom of the formal system or follows from previous members of the sequence by a valid rule of inference.
Gentzen’s consistency proof for PA employs a reduction procedure \(\cR\) on proofs P of the empty sequent together with an assignment ord of representations for ordinals to proofs such that \(\ord(\cR(P))< \ord(P)\). Here \(<\) denotes the ordering on ordinal representations induced by the ordering of the pertinent ordinals. For this purpose he needed representations for ordinals \(<\varepsilon_0\) where \(\varepsilon_0\) is the smallest ordinal \(\tau\) such that whenever \(\alpha<\