Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-23T03:59:24.684Z Has data issue: false hasContentIssue false
  • English
  • Français

A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION

Published online by Cambridge University Press:  13 September 2010

JAN VON PLATO
JAN VON PLATO*
Affiliation:
Department of Philosophy, University of the Helsinki
*
*DEPARTMENT OF PHILOSOPHY, UNIVERSITY OF HELSINKI, 00014 U. OF HELSINKI, FINLAND. E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Gentzen’s thesis proved the equivalence of natural deduction, sequent calculus, and axiomatic logic through a cycle of translations. Mysteriously, even normal derivations in natural deduction got translated into sequent derivations with cuts. It is shown that the insertion of special cuts, whenever left conjunction, left implication, or left universal quantification in sequent calculus is used, results in sequent calculus derivations isomorphic to those in Gentzen’s natural deduction. Thereby the appearance of the cuts in translation is explained.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 4 , Issue 1 , March 2011 , pp. 43 - 53
Copyright
Copyright © Association for Symbolic Logic 2010

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

BIBLIOGRAPHY

Gentzen, G. (1934–1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 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, 4, 19–44.Google Scholar
Gentzen, G. (1969). In Szabo, M., editor. The Collected Papers of Gerhard Gentzen. North-Holland.Google Scholar
Gentzen, G. (2008). The normalization of derivations. The Bulletin of Symbolic Logic, 14, 245–257.Google Scholar
Menzler-Trott, E. (2007). Logic’s Lost Genius: The Life of Gerhard Gentzen. Providence, RI: AMS.Google Scholar
Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge, UK.Google Scholar
von Plato, J. (2001a). Natural deduction with general elimination rules. Archive for Mathematical Logic, 40, 541–567.CrossRefGoogle Scholar
von Plato, J. (2001b). A proof of Gentzen’s Hauptsatz without multicut. Archive for Mathematical Logic, 40, 9–18.Google Scholar
von Plato, J. (2003). Translations from natural deduction to sequent calculus. Mathematical Logic Quarterly, 49, 435–443.CrossRefGoogle Scholar
von Plato, J. (2008). Gentzen’s proof of normalization for intuitionistic natural deduction. The Bulletin of Symbolic Logic, 14, 240–244.CrossRefGoogle Scholar
von Plato, J. (2009). Gentzen’s logic. In Gabbay, D., and Woods, J., editors. Handbook of the History of Logic, Vol. 5. pp. 667–721.Google Scholar
Pottinger, G. (1977). Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12, 323–357.Google Scholar
Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Stockholm, Sweden: Almqvist & Wicksell.Google Scholar
Troelstra, A., & Schwichtenberg, H. (2000). Basic Proof Theory (second edition). Cambridge, UK.Google Scholar
Zucker, J. (1974). Cut-elimination and normalization. Annals of Mathematical Logic, 7, 1–112.Google Scholar