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

Bulletin of Symbolic Logic 18 (3):313-367 (2012)
  Copy   BIBTEX

Abstract

Gentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934—35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,726

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Translations from natural deduction to sequent calculus.Jan von Plato - 2003 - Mathematical Logic Quarterly 49 (5):435.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Gentzen's Proof of Normalization for Natural Deduction.Jan von Plato & G. Gentzen - 2008 - Bulletin of Symbolic Logic 14 (2):240 - 257.
Gentzen's proof of normalization for natural deduction.Jan von Plato - 2008 - Bulletin of Symbolic Logic 14 (2):240-257.
Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs.Paolo Mancosu, Sergio Galvan & Richard Zach - 2021 - Oxford: Oxford University Press. Edited by Sergio Galvan & Richard Zach.

Analytics

Added to PP
2012-08-14

Downloads
103 (#169,543)

6 months
28 (#132,524)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jan Von Plato
University of Helsinki

Citations of this work

Focusing Gentzen’s LK Proof System.Chuck Liang & Dale Miller - 2024 - In Thomas Piecha & Kai F. Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics. Springer. pp. 275-313.
Normal derivability in classical natural deduction.Jan Von Plato & Annika Siders - 2012 - Review of Symbolic Logic 5 (2):205-211.
Eight Inference Rules for Implication.Michael Arndt - 2019 - Studia Logica 107 (4):781-808.
Necessity of Thought.Cesare Cozzo - 2015 - In Heinrich Wansing (ed.), Dag Prawitz on Proofs and Meaning. Cham, Switzerland: Springer. pp. 101-20.

View all 15 citations / Add more citations

References found in this work

Grundzüge der theoretischen Logik.D. Hilbert & W. Ackermann - 1928 - Annalen der Philosophie Und Philosophischen Kritik 7:157-157.
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
Introduction to Metamathematics.Ann Singleterry Ferebee - 1968 - Journal of Symbolic Logic 33 (2):290-291.
Investigations into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.

View all 23 references / Add more references