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

Jan Von Plato
University of Helsinki
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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/bsl/1344861886
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,379
Through your library

References found in this work BETA

Grundzüge der theoretischen Logik.D. Hilbert & W. Ackermann - 1928 - Annalen der Philosophie Und Philosophischen Kritik 7:157-157.
Investigations Into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.

View all 23 references / Add more references

Citations of this work BETA

Normal Derivability in Classical Natural Deduction.Jan Von Plato & Annika Siders - 2012 - Review of Symbolic Logic 5 (2):205-211.
Necessity of Thought.Cesare Cozzo - 2015 - In Heinrich Wansing (ed.), Dag Prawitz on Proofs and Meaning. Springer. pp. 101-20.
Eight Inference Rules for Implication.Michael Arndt - 2019 - Studia Logica 107 (4):781-808.
Early Structural Reasoning. Gentzen 1932.Enrico Moriconi - 2015 - Review of Symbolic Logic 8 (4):662-679.

View all 13 citations / Add more citations

Similar books and articles

A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Cut as Consequence.Curtis Franks - 2010 - History and Philosophy of Logic 31 (4):349-379.
Varieties of Linear Calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Marginalia on Sequent Calculi.A. S. Troelstra - 1999 - Studia Logica 62 (2):291-303.
On Inversion Principles.Enrico Moriconi & Laura Tesconi - 2008 - History and Philosophy of Logic 29 (2):103-113.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.


Added to PP index

Total views
72 ( #161,644 of 2,519,681 )

Recent downloads (6 months)
2 ( #270,824 of 2,519,681 )

How can I increase my downloads?


My notes