Gerhard Gentzen

Gerhard Gentzen was a German mathematician and logician whose work founded modern proof theory. Studying under David Hilbert and Paul Bernays at Gottingen, Gentzen introduced the formal systems of natural deduction and the sequent calculus in his 1934 and 1935 papers, giving logic new frameworks for representing proofs themselves as mathematical objects that could be systematically analyzed and transformed. Gentzen's cut-elimination theorem, often called his Hauptsatz or main theorem, showed that any proof in the sequent calculus using the cut rule could be transformed into an equivalent proof without it, a result with far-reaching consequences for the structure of formal proofs, later applications of which are central to proof-theoretic semantics. In 1936 Gentzen proved the consistency of Peano arithmetic, using a method of transfinite induction up to a specific infinite ordinal that lay just beyond what arithmetic itself could formalize, a form of consistency result that Kurt Godel's incompleteness theorems had shown could not be obtained by finitary methods internal to arithmetic itself. Gentzen worked as an assistant to Hilbert before the Second World War and died of starvation in a Soviet prison camp in Prague in 1945 after being arrested in the aftermath of the city's uprising.