Mathematical Logic Quarterly 49 (5):435 (2003)

Jan Von Plato
University of Helsinki
Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut-free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut-free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains the cuts in Gentzen's translation. Likewise, it is shown that Prawitz' translation contains an implicit process of cut elimination.
Keywords sequent calculus  Natural deduction  cut rule
Categories (categorize this paper)
DOI 10.1002/malq.200310047
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,512
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Necessity of Thought.Cesare Cozzo - 2015 - In Heinrich Wansing (ed.), Dag Prawitz on Proofs and Meaning. Springer. pp. 101-20.
Natural Deduction Bottom Up.Ernst Zimmermann - 2021 - Journal of Logic, Language and Information 30 (3):601-631.

View all 9 citations / Add more citations

Similar books and articles

Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Varieties of Linear Calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
Towards a More General Concept of Inference.Ivo Pezlar - 2014 - Logica Universalis 8 (1):61-81.
Natural Deduction Systems for Nelson's Paraconsistent Logic and its Neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A Problem of Normal Form in Natural Deduction.Jan von Plato - 2000 - Mathematical Logic Quarterly 46 (1):121-124.
A Normalizing System of Natural Deduction for Intuitionistic Linear Logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.


Added to PP index

Total views
39 ( #293,309 of 2,520,901 )

Recent downloads (6 months)
1 ( #405,457 of 2,520,901 )

How can I increase my downloads?


My notes