Gentzen ordinal reduction for arithmetic

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 math.stanford.edu/~feferman/papers/reductive.pdf .