Studia Logica 107 (1):195-231 (2019)

Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only of \- and \-equations. On the basis of the categorial interpretation of NI\, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting NI\-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s11225-017-9772-6
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: 69,979
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

Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 1965 - Stockholm, Sweden: Dover Publications.
A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.

View all 6 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
Translations From Natural Deduction to Sequent Calculus.Jan von Plato - 2003 - Mathematical Logic Quarterly 49 (5):435.
Expressive Power and Incompleteness of Propositional Logics.James W. Garson - 2010 - Journal of Philosophical Logic 39 (2):159-171.
Normal Deduction in the Intuitionistic Linear Logic.G. Mints - 1998 - Archive for Mathematical Logic 37 (5-6):415-425.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
A Binary-Conclusion Natural Deduction System.K. Fujita - 1999 - Logic Journal of the IGPL 7 (4):517-545.
Natural Deduction for First-Order Hybrid Logic.Torben BraÜner - 2005 - Journal of Logic, Language and Information 14 (2):173-198.
Substructural Logics in Natural Deduction.Ernst Zimmermann - 2007 - Logic Journal of the IGPL 15 (3):211-232.
Natural Deduction for Bi-Intuitionistic Logic.Luca Tranchini - 2017 - Journal of Applied Logic 25:S72-S96.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A Normalizing System of Natural Deduction for Intuitionistic Linear Logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.


Added to PP index

Total views
34 ( #334,834 of 2,504,871 )

Recent downloads (6 months)
2 ( #277,627 of 2,504,871 )

How can I increase my downloads?


My notes