Gentzen, Gerhard
Gentzen, Gerhard
(b. Creifswald, Germany, 24 November 1909; d. Prague, Czechoslovakia, 4 August 1945)
logic, foundations of mathematics.
Gentzen was a born mathematician. As a boy he declared his dedication to mathematics, and his short life constituted a realization of that promise. He benefited from the teaching of such renowned scholars as P. Bernays, C. Carathéodory, R. Courant, D. Hilbert; A. Kneser, E. Landau, and H, Weyl and at the age of twenty-three, three, received his doctorate in mathematics. In 1934 he became one of Hilbert’s assistants and held that position until 1943, with the exception of a two-year period of compulsory military service from 1939 to 1941, when he was requested to take up a teaching post at the University of Prague. He died at Prague of malnutrition three months after his internment by the liberating authorties in May 1945.
Genzen combined in rare measure an exceptional inventiveness and the talent for coordinating diverse existing knowledge into a systematic conceptual framework. He invented “natural deduction” in order to create a predicate logic more akin to actual mathematical reasoning than the Frege-Russell-Hilbert systems, then used P. Hertz’s “sentences” to transform his natural calculus, into a “calculus of Sequents’Thus he succeeded in making classical logic appear as a simple extension of intuitionist logic and in enunciating his Hauptsatz (chief theory), which he had discovered while studying more closely the specific properties of natural deduction. A formalization of elementary number theory based on sequents and his ingenious idea of using restricted transfinite induction as a metamathematical technique enabled Gentzen to carry out the first convincing consistency proof for elementary number theory, in spite of the limitations imposed on such proofs by Gödel’s theorem. He eventually proved directly the nonderivability in elementary number theory of the required transfinite induction up to έ0. In view of subsequent developments, Gentzen’s consistency proof must be considered as the most outstanding single contribution to Hilbert’s program.
The Hauptsatz says that in both intuitionist and classical predicate logic, a purely logical sequent can be proved without “cut” (modus ponens, in Hilberttype systems). A corollary is the subformula property, to the effect that the derivation formulas in a cut-free proof are compounded in the sequent proved. This entails, for example, the consistency of classical and intuitionist predicate logic, the decidability of intuitionidt prepositional logic, the nonderivability of the law of the excluded middle in intuitionist predicate logic. Gentzen succeeded in sharpening the Hauptsatz for classical logic to the midsequent theorem (Herbran-Gentzen theorem) for sequents whose formulas are prenex, by proving that any such sequent has a cut-free proof consisting of two parts, the first part quantifier-free and the second consisting essentially of instances of quantification. The last quantifier-free sequent in the proof is the “midsequent” and corresponds closely to a “Herbrand tautology.”
Among the consequences of the midsequent theorem are the consistency of arithmetic without induction, Craig’s interpolation lemma, and Beth’s definability theorem. Recent extensions of the Houptsatz to stronger deductive systems, including infinitary logic, have yielded partial results at the second stage of Hilbert’s program in the form of consistency proofs for subsystems of classical analysis. Only a few days before his death. Gentzen had in fact announced the feasibility of a consistency proof for classical analysis as a whole.
BIBLIOGRAPHY
Gentzen’s writings include. “Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen,” in Mathematische Annalen,107 (1932), 329-350; “Untersuchungen über das logische Schliessen,” in Mathematische Zeitschrift, 39 (1935), 176-210, 405-431, his inaugural dissertation, submitted to the Faculty of Mathematics and Natural Science of the University of Göttingen in the summer of 1933; “Die Widerspruchsfreiheit der reinen Zablentheorie,” in Mathematische Annalen, 112 (1936), 493-565; “Die Widerspruchsfreiheit der Stufenlogik,” in Mathematische Zeitschrift, 41 no. 3 (1936), 357-366; “Der Unendlichkeitsbegrift in derMathematik,” in Semester-Berichte, Münster on Westphalem, 9th semster (Winter 1936/1937), pp. 65-80; “Unendlichkeitsbegriff und Widerspruchsfreiheit der Mathematik,” in Travaux du IXe Congrés International de Philosophie, VI (Paris, 1937), 201-205; “Die gegenwärtige Lage in der mathematischen Grundlagenforschung,” in Forschungen zur Logik und zur Grundlegung der exaten Wissenschaftden, n.s. 4 (1938), 5-18, also in Deutsche Mathematik, 3 (l939), 255-268; “Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie,” in Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, n.s. 4 (1938), 19-44; “Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie:” in Mathematische Annalen, 119 , no. 1 (1943), 140-161, his Ph.D. Habilitation thesis, submitted to the Faculty of Mathematics and Natural Science of the University of Göttingen in the summer of 1942; and “Zusammenfassung von mehreren vollständigen Induktionen zu einer einzigen,” in Archiv fü mathematische Logik und Grundlagenforschung, 2 no. 1 (l954), l-3.
For a detailed account of Gentzen’s life, extensive crossreferences to his papers, and a critical appraisal of germane subsequent developments, see M. E. Szabo, Collected Papers of Gerhard Gentzen, in the Series Studies in Logic (Amsterdam, 1969); of particular interest are the-trans of two articles Gentzen submitted to Mathematische Annalen, but withdrew before publication (of which galley proofs are privately owned), “Über das Verhältnis zwischen intuitionistischer und Klassischer Arithmetik” (1933) and sections 4 and 5 of “Die Widerspruchsfreiheit der reinen Zahlentheorie” (1935).
Manfred E. Szabo