Gentzen's Consistency Proof

Gentzen's consistency proof is a result in proof theory, published by Gerhard Gentzen in 1936, showing that the Peano axioms of first-order arithmetic contain no contradiction, provided that a separate system used in the argument is itself free of contradictions. That auxiliary system, primitive recursive arithmetic extended with quantifier-free transfinite induction up to the ordinal epsilon-naught, is neither weaker nor stronger than the Peano axioms, but Gentzen argued it avoids certain questionable modes of inference and so its own consistency is less controversial.