Natural Deduction for Full S5 Modal Logic with Weak Normalization

Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [Prawitz, D., “Natural Deduction: A Proof-theoretical Study”, Stockholm Studies in Philosophy 3, Almqvist and Wiksell, Stockholm, 1965] from a proof-theoretical perspective. Prawitz proved weak normalization for classical logic just for a language without ∨, ∃ and with a restricted application of reduction ad absurdum. Reduction steps related to ∨, ∃ and classical negation brings about a lot of problems solved only rather recently [Seldin, J., Normalization and Excluded Middle I, Studia Logica 48 (1989), 193–217; Stalmark, G., Normalizations Theorems for Full First Order Classical Natural Deduction, The Journal of Symbolic Logic 56 (1991); Massi, C.D.B., “Provas de Normalização para a Lógica Clássica”, Ph.D. thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990; Pereira, L.C., and C.D.B. Massi, Normalização para a Lógica Clássica, O que nos faz pensar, Cadernos de Filosofia da PUC-RJ 2 (1990), 49–53]. For classical S4/S5 modal logics, Prawitz defined normalizable systems, but for a language without ∨, ∃ and ◊. We can mention cut-free Gentzen systems for S4/S5 [Meré, M.C., and L.C. Pereira. “A New Cut-Free System for Intuitionistic S4”, Encontro Brasileiro de Lógica, Salvador, 1996; Mints, G.E., “Lewis' Systems and System T (1965–1973)”, Selected Papers in Proof Theory, Studies in Proof Threory, North-Holland, 1992, 221–293; Mints, G.E., Cut-Free Calculi of the S5 Type Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics 8 (1970), 79–82; Bragança, R.C.M., E.H. Haeusler, and L.C. Pereira, A New Cut-Free Sequent calculus for S5, The Bulletin of Symbolic Logic 5 (1999), 497–498; Braüner, T., A Cut-Free Gentzen Formulation of the Modal Logic S5, Logic Journal of the IGPL 8 (2000), 629–643; H. Wansing. Sequent Calculi for Normal Modal Propositional Logics, Journal of Logic and Computation 4 (1994), 125–142], normalizable natural deduction systems for intuitionistic modal logics [Simpson, A.K., “The Proof Theory and Semantics of Intuitionistic Modal Logic”, Ph.D. thesis, University of Edinburgh, 1994; Masini, A., 2-Sequent Calculus: Intuitionism and Natural Deduction, Journal of Logic and Computation 3 (1993), 533–562] and for full classical S4 [Martins, L.R., and A.T. Martins, “Normalizable Natural Deduction Rules for S4 Modal Operators”, World Congress on Universal Logic, Montreux, 2005, 79–80], but not for full classical S5. Here our focus is in the definition of a classical and normalizable natural deduction system for S5, taken not only □ and ◊ as primitive symbols, but also all connectives and quantifiers, including classical negation, disjunction and the existential quantifier. The normalization procedure will be based on the strategy proposed by [Massi, C.D.B., “Provas de Normalização para a Lógica Clássica”, Ph.D. thesis, Departamento de Filosofia, UNICAMP, Campinas, 1990; Pereira, L.C., and C.D.B. Massi, Normalização para a Lógica Clássica, O que nos faz pensar, Cadernos de Filosofia da PUC-RJ 2 (1990), 49–53] to cope with the combined use of classical negation, ∨ and ∃. We will extend such results to deal with ◊ too. The elimination rule for ◊ will use the notions of connection and of essentially modal formulas already proposed by Prawitz for the introduction of □. Weak normalization and subformula property is proved for full S5.