= Gentzen ordinal reduction for arithmetic
{c}
Gentzen's consistency argument associates finite arithmetic derivations with effective <ordinal> notations below <epsilon zero>. An alleged contradiction admits an effective proof reduction preserving the contradictory end-sequent and strictly decreasing the assigned ordinal. Termination would therefore produce a normal contradiction, excluded by inspection of the logical rules and true atomic axioms. This explains why the relevant <transfinite induction> principle implies <formal consistency statement>. For a finite slow-well-ordering formulation one additionally needs the controlled-termination miniaturization theorem, rather than assuming that ordinary proof reductions have linearly growing size. The reduction program is discussed in https://math.stanford.edu/~feferman/papers/reductive.pdf .
Back to article page
