Studia Logica 96 (1):95-108 (2010)

Edward Haeusler
Pontifícia Universidade Católica do Rio de Janeiro
The introduction and elimination rules for material implication in natural deduction are not complete with respect to the implicational fragment of classical logic. A natural way to complete the system is through the addition of a new natural deduction rule corresponding to Peirce's formula → A) → A). E. Zimmermann [6] has shown how to extend Prawitz' normalization strategy to Peirce's rule: applications of Peirce's rule can be restricted to atomic conclusions. The aim of the present paper is to extend Seldin's normalization strategy to Peirce's rule by showing that every derivation Π in the implicational fragment can be transformed into a derivation Π' such that no application of Peirce's rule in Π' occurs above applications of →-introduction and →-elimination. As a corollary of Seldin's normalization strategy we obtain a form of Glivenko's theorem for the classical {→}-fragment.
Keywords Philosophy   Computational Linguistics   Mathematical Logic and Foundations   Logic
Categories (categorize this paper)
DOI 10.1007/s11225-010-9275-1
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: 63,339
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

On the Proof Theory of the Intermediate Logic MH.Jonathan P. Seldin - 1986 - Journal of Symbolic Logic 51 (3):626-647.
Normalization and Excluded Middle. I.Jonathan P. Seldin - 1989 - Studia Logica 48 (2):193 - 217.
On Cut Elimination in the Presence of Perice Rule.Lev Gordeev - 1987 - Archive for Mathematical Logic 26 (1):147-164.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Contraction-Elimination for Implicational Logics.Ryo Kashima - 1997 - Annals of Pure and Applied Logic 84 (1):17-39.
On the EA-Fragment of Classical Propositional Logic.Janis Cirulis - 1981 - Bulletin of the Section of Logic 10 (4):158-160.
Natural Deduction Systems for Some Non-Commutative Logics.Norihiro Kamide & Motohiko Mouri - 2007 - Logic and Logical Philosophy 16 (2-3):105-146.


Added to PP index

Total views
28 ( #390,118 of 2,448,787 )

Recent downloads (6 months)
1 ( #444,630 of 2,448,787 )

How can I increase my downloads?


My notes