Gerhard Gentzen

Gerhard Gentzen was a German logician who studied and worked at Göttingen in the circle of David Hilbert and died in Prague at the end of the Second World War. His 'Investigations into Logical Deduction' introduced natural deduction and the sequent calculus, which model logical reasoning by rules for introducing and eliminating connectives, and proved the cut-elimination theorem. He also gave a consistency proof for arithmetic using transfinite induction, founding structural proof theory.

Key ideas

• Natural deduction captures logical reasoning through paired rules for introducing and eliminating each connective.
• In the sequent calculus, any proof using the cut rule can be transformed into one without it (the Hauptsatz).
• The consistency of arithmetic can be proved using transfinite induction up to the ordinal epsilon-zero.
• The meaning of a logical constant can be seen as given by its introduction rules.

Major works

• "Investigations into Logical Deduction" (Untersuchungen über das logische Schließen, 1934–1935)
• "The Consistency of Elementary Number Theory" (Die Widerspruchsfreiheit der reinen Zahlentheorie, 1936)

In the conversation

• Question Every invoice needs some approver: why does the order of quantifiers change the meaning? Harpreet Kaur Grewal · 4 replies