There exists a reduction procedure R on proofs P of the empty sequent together with an assignment ord of ordinal representations to proofs such that ord(R(P)) < ord(P).
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<\