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: 62,513
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.
Relevance Logic.Michael Dunn & Greg Restall - 2002 - In D. Gabbay & F. Guenthner (eds.), Handbook of Philosophical Logic. Kluwer Academic Publishers.
Curry's Paradox.Robert K. Meyer, Richard Routley & J. Michael Dunn - 1979 - Analysis 39 (3):124 - 128.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
A General Logic.John Slaney - 1990 - Australasian Journal of Philosophy 68 (1):74 – 88.

View all 10 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 7 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
42 ( #253,661 of 2,446,472 )

Recent downloads (6 months)
3 ( #231,676 of 2,446,472 )

How can I increase my downloads?

Downloads

My notes