Gentzen's proof systems: byproducts in a work of genius (Q2915886)

By analysing Gentzen's handwritten manuscripts, the author traces the origin of the natural deduction system and the sequent calculus. These systems, consisting of inference rules arranged in tree form, make analysis of proofs possible, unlike previous linear forms with (logical) axioms. Gentzen got `the new, simple, and right idea' that the author compares to Einstein's about Brownian motion. He first summarizes logic activities in the 1920s, just before Gentzen came on the scene. His first document, ``Five forms of natural calculi'', is dated September 23, 1932. The handwritten version of the thesis, written soon after, bears the same title, ``Untersuchungen über das logische Schließen'', as the published version in [Math. Z. 39, 176--210 (1934; Zbl 0010.14501; JFM 60.0020.02); ibid. 39, 405--431 (1934; Zbl 0010.14601; JFM 60.0846.01)]. But its aim was to give a consistency proof of arithmetic. It was not easy to achieve, and the published version is solely about pure logic. Normalization works for intuitionistic natural deduction, but not for classical. This is one of two motivations for inventing sequent calculus. The other is translations between a natural deduction and an axiomatic system (Hilbert-Ackermann's, in particular), where arrow is understood to be derivability. Apparently, the author did not come across the origin of sequents with many formulas in their succedents. (`Without further explanation' such sequents appear in the thesis manuscript, he states.) This is a real pity, because it must have been very exciting and even mysterious to discover that this simple device gives complete symmetry and distinguishes intuitionistic and classical systems so neatly. The author goes through later work of Gentzen, and other people's -- particularly Bernays' -- subsequent work including ``to appear'' articles. At places he proceeds through a systematic study, making the paper `history of logic with theorems'.NEWLINENEWLINE Besides these historical and mathematical accounts, the author talks about the difficult social situation of the 1930s and loss of many manuscripts in the 1970s. He also gives his personal accounts of ``discovering'' the manuscript thesis in 2005: an excited (the reviewer's guess) phone call to Prawitz and his `cool reply', and so forth.