Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus

Andrzej Indrzejczak

doi:10.18778/0138-0680.45.2.05

Authors

Andrzej Indrzejczak University of Łódź, Department of Logic

DOI:

https://doi.org/10.18778/0138-0680.45.2.05

Keywords:

Modal logic S5, decidability, normal forms, sequent calculus

Abstract

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi (SC) for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form.

References

[1] A. Avron, A Constructive Analysis of RM, Journal of Symbolic Logic 52 (1987), pp. 939–951.
Google Scholar

[2] A. Avron, The method of hypersequents in the proof theory of propositional non-classical logic, [in:] W. Hodges, M. Hyland, C. Steinhorn, and J. Strauss, editors, Logic: from Foundations to Applications, Oxford University Press, Oxford (1996), pp. 1–32.
Google Scholar

[3] K. Bednarska and A. Indrzejczak, Hypersequent calculi for S5 - the methods of cut elimination, Logic and Logical Philosophy 24/3 (2015), pp. 277–311.
Google Scholar

[4] N. D. Belnap, Display Logic, Journal of Philosophical Logic 11(1982), pp. 375–417.
Google Scholar

[5] T. Braüner, A cut-free Gentzen formulation of the modal logic S5, Logic Journal of the IGPL 8 (2000), pp. 629–643.
Google Scholar

[6] T. Brünnler, A cut-free Gentzen formulation of the modal logic S5, Logic Journal of the IGPL 8 (2000), pp. 629–643.
Google Scholar

[7] R. Carnap, Modalities nad quantification, Journal of Symbolic Logic 11 (1946), pp. 33–64.
Google Scholar

[8] L. Farinas del Cerro and A. Herzig, Modal Deduction with Applications in Epistemic and Temporal Logics, [in:] D. Gabbay et all. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. IV, Clarendon Press, Oxford 1995, pp. 499–594.
Google Scholar

[9] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983.
Google Scholar

[10] M. Fitting, Simple propositional S5 tableau system, Annals of Pure and Applied Logic 96 (1999), pp. 101–115.
Google Scholar

[11] R. Goré, Tableau Methods for Modal and Temporal Logics, [in:] M. D’Agostino et al. (eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht 1999, pp. 297–396.
Google Scholar

[12] G. E. Hughes, M. J. Cresswell, A New Introduction to Modal Logic, Routledge, London 1996.
Google Scholar

[13] A. Indrzejczak, Cut-free double sequent calculus for S5, Logic Journal of the IGPL 6 (1998), pp. 505–516.
Google Scholar

[14] S. Kanger, Provability in Logic, Almqvist & Wiksell, Stockholm 1957.
Google Scholar

[15] S. Kripke, Semantical Analysis of Modal Logic I, Zeitschrift f¨ur Mathematische Logik und Grundlegen der Mathematik 9 (1963), pp. 67–96.
Google Scholar

[16] H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence, Springer 2014, pp. 51–68.
Google Scholar

[17] O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, [in:] Proceedings of LICS, Springer 2013, pp. 408–417.
Google Scholar

[18] B. Lellmann, D. Pattinson, Correspondence between Modal Jilbert Axioms and Sequent Rules with an Application to S5, [in:] D. Galmiche, D. Larchey-Wendling (eds.), TABLEAUX 2013. LNCS, vol. 8132, Springer 2013, pp. 219–233.
Google Scholar

[19] G. Mints, Cut-free calculi of the S5 type, Studies in Constructive Mathematics and Mathematical Logic II (1970), pp. 79–82.
Google Scholar

[20] S. Negri, Proof Analysis in Modal Logic, Journal of Philosophical Logic 34 (2005), pp. 507–544.
Google Scholar

[21] M. Ohnishi, K. Matsumoto, Gentzen Method in Modal Calculi I, Osaka Mathematical Journal 9 (1957), pp. 113–130.
Google Scholar

[22] M. Ohnishi, K. Matsumoto, Gentzen Method in Modal Calculi II, Osaka Mathematical Journal 11 (1959), pp. 115–120.
Google Scholar

[23] F. Poggiolesi, A Cut-free Simple Sequent Calculus for Modal Logic S5, Review of Symbolic Logic 1 (2008), pp. 3–15.
Google Scholar

[24] F. Poggiolesi, Reflecting the semantic features of S5 at the syntactic level, [in:] New Essays in Logic and Philosophy of Science, M. D’Agostino, G. Giorell, F. Laudisa, T. Pievani, C. Singaglia (eds.), London College Publications, 2010, pp. 13–25.
Google Scholar

[25] F. Poggiolesi, Gentzen Calculi for Modal Propositional Logic, Springer 2011.
Google Scholar

[26] G. Pottinger, Uniform cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic 48 (1983), p. 900.
Google Scholar

[27] D. Prawitz, Natural Deduction, Almqvist and Wiksell, Stockholm 1965.
Google Scholar

[28] G. Restall, Proofnets for S5: sequents and circuits for modal logic, [in:] Lecture Notes in Logic 28 (2007), pp. 151–172.
Google Scholar

[29] M. Sato, A Study of Kripke-type Models for Some Modal Logics by Gentzen’s Sequential Method, Publications of the Research Institute for Mathematical Sciences, Kyoto University 1977, 13, pp. 381–468.
Google Scholar

[30] T. Skura, Refutation methods in propositional modal logics, Semper 2013.
Google Scholar

[31] P. Stouppa, The design of modal proof theories: the case of S5, Master Thesis, Dresden 2004.
Google Scholar

[32] P. Stouppa, A deep inference system for the modal logic S5, Studia Logica 85 (2007), pp. 199–214.
Google Scholar

[33] M. Takano, Subformula Property as a substitute for Cut-Elimination in Modal Propositional Logics, Mathematica Japonica 37/6 (1992), pp. 1129–1145.
Google Scholar

[34] M. Wajsberg, Ein erweiteter Klassenkalkül, Monatshefte f¨ur Mathematik unf Physik 40 (1933), pp. 113–126.
Google Scholar

[35] H. Wansing, Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999.
Google Scholar

[36] J. J. Zeman, Modal Logic, Oxford University Press, Oxford 1973.
Google Scholar