Gerhard Gentzen

Solution Preview

At age 22 in 1932, Gentzen submitted paper #1: "On the Existence of Independent Axiom Systems for Infinite Sentence Systems." He introduces a system of the propositional calculus as a sequent calculus based on Hertz's work. He modifies Hertz's "syllogism" rule to be Gentzen's "cut" rule. In this context he constructs an infinite set of sentences that has no independent set of axioms. He also shows that all "linear" sentence systems do have an independent axiomatization.
Gentzen classifies mathematics into three levels (a classification which goes back to Weyl [1931]) based on how infinity is used: elementary number theory, analysis and general set theory. ...