Studia Logica 102 (6):1143-1166 (2014)

Authors
Greg Restall
University of Melbourne
Abstract
Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which differs again in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems.
Keywords Natural deduction  Normal proof  Sequent calculus  Structural rule  Proof net
Categories (categorize this paper)
DOI 10.1007/s11225-014-9598-4
Options
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: 52,956
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

Display Logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
A Brief History of Natural Deduction.Francis Jeffry Pelletier - 1999 - History and Philosophy of Logic 20 (1):1-31.
Curry's Paradox.Robert K. Meyer, Richard Routley & J. Michael Dunn - 1979 - Analysis 39 (3):124 - 128.
A General Logic.John Slaney - 1990 - Australasian Journal of Philosophy 68 (1):74 – 88.

View all 9 references / Add more references

Citations of this work BETA

Contraction and Revision.Shawn Standefer - 2016 - Australasian Journal of Logic 13 (3):58-77.
Natural Deduction for Bi-Intuitionistic Logic.Luca Tranchini - 2017 - Journal of Applied Logic 25:S72-S96.

View all 6 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.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
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.
Uniqueness of Normal Proofs in Implicational Intuitionistic Logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.

Analytics

Added to PP index
2014-12-02

Total views
38 ( #254,282 of 2,343,995 )

Recent downloads (6 months)
1 ( #514,126 of 2,343,995 )

How can I increase my downloads?

Downloads

My notes