Skip to main content

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.


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

Cite this article
Pick a style below, and copy the text for your bibliography.

  • MLA
  • Chicago
  • APA

"Gentzen, Gerhard." Complete Dictionary of Scientific Biography. . 22 Apr. 2019 <>.

"Gentzen, Gerhard." Complete Dictionary of Scientific Biography. . (April 22, 2019).

"Gentzen, Gerhard." Complete Dictionary of Scientific Biography. . Retrieved April 22, 2019 from

Learn more about citation styles

Citation styles gives you the ability to cite reference entries and articles according to common styles from the Modern Language Association (MLA), The Chicago Manual of Style, and the American Psychological Association (APA).

Within the “Cite this article” tool, pick a style to see how all available information looks when formatted according to that style. Then, copy and paste the text into your bibliography or works cited list.

Because each style has its own formatting nuances that evolve over time and not all information is available for every reference entry or article, cannot guarantee each citation it generates. Therefore, it’s best to use citations as a starting point before checking the style against your school or publication’s requirements and the most-recent information available at these sites:

Modern Language Association

The Chicago Manual of Style

American Psychological Association

  • Most online reference entries and articles do not have page numbers. Therefore, that information is unavailable for most content. However, the date of retrieval is often important. Refer to each style’s convention regarding the best way to format page numbers and retrieval dates.
  • In addition to the MLA, Chicago, and APA styles, your school, university, publication, or institution may have its own requirements for citations. Therefore, be sure to refer to those guidelines when editing your bibliography or works cited list.