From hauptsatz to hilfssatz

Abstract

Gentzen found his original consistency proof of arithmetic late in 1934. His work in pure logic was a preliminary to the result. Archival sources show that the consistency proof was based on an explicit semantic notion of correctness as reducibility of sequents and a proof that steps of derivation maintain reducibility. A crucial point in the latter was Gentzen’s Hilfssatz that stated, in analogy to his famous Hauptsatz, that composition of sequents maintains reducibility. The Hilfssatz was needed essentially for the case of the rule of complete induction. It was the point at which Gentzen’s proof superseded standard arithmetic methods in favour of an induction on well-founded trees, i.e., what came later to be called bar induction. After criticisms by Bernays and Gödel, the first proof evolved into one based on transfinite induction. Traces of the Hilfssatz that was founded on intuitionistic ideas disappeared, and Gentzen developed instead transfinite induction further into a general ordinal proof theory.