The ordinals less than epsilon_0 are well-founded (there is no infinite strictly descending sequence of ordinals below epsilon_0).

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<\