Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-12-03T19:05:20.165Z Has data issue: false hasContentIssue false
  • English
  • Français

Gentzen's Proof of Normalization for Natural Deduction

Published online by Cambridge University Press:  15 January 2014

Jan von Plato
Jan von Plato*
Affiliation:
Department of philosophy P.O. box 24 00014, University of Helsinki, FinlandE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Gentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen (Investigations into logical reasoning) that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the sequents have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.

We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 14 , Issue 2 , June 2008 , pp. 240 - 257
Copyright
Copyright © Association for Symbolic Logic 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Bernays, P. [1936], Logical calculus, The Institute for Advanced Study, Princeton.Google Scholar
Bernays, P. [1965], Betrachtungen zum Sequenzen-kalkul, Contributions to Logic and Methodology in honor of J. M. Bochenski, North-Holland, Amsterdam, pp. 1–44.Google Scholar
Bernays, P. [1970], On the original Gentzen consistency proof for number theory, Intuitionism and proof theory (Myhill, J. et al., editors), North-Holland, Amsterdam, pp. 409–417.Google Scholar
Gentzen, G. [1933], Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik, submitted to Mathematische Annalen on 15 March 1933 but withdrawn, published in Archiv für mathematische Logik , vol. 16 (1974), pp. 119–132.Google Scholar
Gentzen, G. [1934–1935], Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39, pp. 176–210 and 405–431.CrossRefGoogle Scholar
Gentzen, G. [1938], Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, vol. 4, pp. 19–44.Google Scholar
Gentzen, G. [1969], The collected papers of Gerhard Gentzen (Szabo, M., editor), North-Holland, Amsterdam.Google Scholar
Gödel, K. [1933], Zur intuitionistischen Arithmetik und Zahlentheorie, as reprinted in Gödel [1986], pp. 286–295.Google Scholar
Gödel, K. [1986, 1990, 1995, 2003], Collected works I–V, Oxford University Press.Google Scholar
Hilbert, D. [1931], Die Grundlegung der elementaren Zahlenlehre, Mathematische Annalen, vol. 104, pp. 485–494.CrossRefGoogle Scholar
Hilbert, D. and Ackermann, W. [1928], Grundzüge der theoretischen Logik, Springer.Google Scholar
Mentzler-Trott, E. [2007], Logic's lost genius: The life of Gerhard Gentzen, American Mathematical Society, Providence, Rhode Island.Google Scholar
Von Plato, J. [2008], Gentzen's logic, Handbook of the History and Philosophy of Logic (Gabbay, D. and Woods, J., editors), Elsevier, in press.Google Scholar
Prawitz, D. [1965], Natural deduction: A proof-theoretical study, Almqvist & Wicksell, Stockholm.Google Scholar
Raggio, A. [1965], Gentzen's Hauptsatz for the systems NI and NK, Logique et analyse, vol. 8, pp. 91–100.Google Scholar
Troelstra, A. and Schwichtenberg, H. [2000], Basic proof theory, 2 ed., Cambridge.Google Scholar