Archive for Mathematical Logic 40 (7):541-567 (2001)

Jan Von Plato
University of Helsinki
The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only
Keywords Legacy
Categories (categorize this paper)
DOI 10.1007/s001530100091
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: 64,077
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

Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1975 - Journal of Symbolic Logic 40 (2):232-234.
Die Widerspruchsfreiheit der Reinen Zahlentheorie.Gerhard Gentzen - 1936 - Journal of Symbolic Logic 1 (2):75-75.

Add more references

Citations of this work BETA

General-Elimination Harmony and the Meaning of the Logical Constants.Stephen Read - 2010 - Journal of Philosophical Logic 39 (5):557-576.
A Note on Harmony.Nissim Francez & Roy Dyckhoff - 2012 - Journal of Philosophical Logic 41 (3):613-628.
Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.

View all 40 citations / Add more citations

Similar books and articles

A Normalizing System of Natural Deduction for Intuitionistic Linear Logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Normal Derivations and Sequent Derivations.Mirjana Borisavljevi - 2008 - Journal of Philosophical Logic 37 (6):521 - 548.
Varieties of Linear Calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
A Problem of Normal Form in Natural Deduction.Jan von Plato - 2000 - Mathematical Logic Quarterly 46 (1):121-124.
A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Harmonising Natural Deduction.Hartley Slater - 2008 - Synthese 163 (2):187 - 198.
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
35 ( #311,449 of 2,454,555 )

Recent downloads (6 months)
1 ( #449,188 of 2,454,555 )

How can I increase my downloads?


My notes