Annals of Pure and Applied Logic 152 (1):132-147 (2008)

Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [D. Prawitz, Natural Deduction: A Proof-theoretical Study, in: Stockholm Studies in Philosophy, vol. 3, Almqvist and Wiksell, Stockholm, 1965. Reprinted at: Dover Publications, Dover Books on Mathematics, 2006] from a proof-theoretical perspective. Prawitz proved weak normalization for classical logic only for a language without logical or, there exists and with a restricted application of reduction ad absurdum. Reduction steps related to logical or, there exists and classical negation bring about many problems solved only rather recently. For classical S5 modal logic, Prawitz defined a normalizable system, but for a language without logical or, there exists, ◊ and, for a propositional language without ◊, Medeiros [M.da P.N. Medeiros, A new S4 classical modal logic in natural deduction, Journal of Symbolic Logic 71 799–809] presented a normalizable system for classical S4. We can mention many cut-free Gentzen systems for S4, S5 and K45/K45D, some normalizable natural deduction systems for intuitionistic modal logics and one more for full classical S4, but not for full classical S5. Here our focus is on the definition of a classical and normalizable natural deduction system for S5, taking not only □ and ◊ as primitive symbols, but also all connectives and quantifiers, including classical negation, disjunction and the existential quantifier. The normalization procedure is based on the strategy proposed by Massi [C.D.B. Massi, Provas de normalizaçaõ para a lógica clássica, Ph.D. Thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990] and Pereira and Massi [L.C. Pereira, C.D.B. Massi, Normalização para a lógica clássica, in: O que nos faz pensar, Cadernos de Filosofia da PUC-RJ, vol. 2, 1990, pp. 49–53] for first-order classical logic to cope with the combined use of classical negation, disjunction and the existential quantifier. Here we extend such results to deal with □ and ◊ too. The elimination rule for ◊ uses the notions of connection and of essentially modal formulas already proposed by Prawitz for the introduction of □. Beyond weak normalization, we also prove the subformula property for full S5
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2007.11.007
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,323
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

Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
A New S4 Classical Modal Logic in Natural Deduction.Maria Da Paz N. Medeiros - 2006 - Journal of Symbolic Logic 71 (3):799 - 809.
Normalization and Excluded Middle. I.Jonathan P. Seldin - 1989 - Studia Logica 48 (2):193 - 217.
A Cut-Free Gentzen Formulation Of The Modal Logic S5.T. Braüner - 2000 - Logic Journal of the IGPL 8 (5):629-643.

View all 8 references / Add more references

Citations of this work BETA

Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.

Add more citations

Similar books and articles

Natural Deduction Systems for Some Non-Commutative Logics.Norihiro Kamide & Motohiko Mouri - 2007 - Logic and Logical Philosophy 16 (2-3):105-146.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
Atomic Polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
A New S4 Classical Modal Logic in Natural Deduction.Maria Da Paz N. Medeiros - 2006 - Journal of Symbolic Logic 71 (3):799 - 809.
Natural Deduction and Curry's Paradox.Susan Rogerson - 2007 - Journal of Philosophical Logic 36 (2):155 - 179.


Added to PP index

Total views
32 ( #339,538 of 2,448,703 )

Recent downloads (6 months)
1 ( #445,641 of 2,448,703 )

How can I increase my downloads?


My notes