Modal Logic and Ordinary Sequent Calculi

  • Francesca PoggiolesiEmail author
Part of the Trends in Logic book series (TREN, volume 32)


The first part of the chapter is dedicated to a brief summary of the main notions and results of what is usually called normal modal logic. In the second part of the chapter we present the ordinary sequent calculi that have been developed for modal logic. It turns out that these calculi do not satisfy many of the properties of a good sequent calculus. In the last section we begin to consider how one might generalise the classical sequent calculus.


Modal Logic Sequent Calculus Modal Formula Normal Modal Logic Propositional Letter 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 11.
    P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, Cambridge, 2001.Google Scholar
  2. 14.
    T. Braüner. A cut-free Gentzen formulation of the modal logic S5. Logic Journal of the IGPL, 8:629–643, 2000.CrossRefGoogle Scholar
  3. 27.
    H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249–265, 1952.CrossRefGoogle Scholar
  4. 36.
    R. Feys. Les systèmes formalisés des modalités aristotéliciennes. Revue Philosophique de Louvain, 48:478–509, 1950.CrossRefGoogle Scholar
  5. 37.
    K. Fine. An incomplete logic containing S4. Theoria, 40:23–29, 1974.CrossRefGoogle Scholar
  6. 45.
    L. Goble. Gentzen systems for modal logic. Notre Dame Journal of Formal Logic, 15:455–461, 1974.CrossRefGoogle Scholar
  7. 46.
    R. I. Golblatt and S. K. Thomason. Axiomatic classes in propositional modal logic. In J. Crossley, editor, Algebra and Logic, pp. 163–173. Springer, Dordrecht, 1974.Google Scholar
  8. 47.
    R. Goré. Cut-free Sequent and Tableau Systems for Propositional Normal Modal Logics. Ph.D. Thesis, Technical Report No. 257, University of Cambridge, Cambridge Computer Laboratory, 1992.Google Scholar
  9. 50.
    R. Goré and R. Ramanayake. Valentini’s cut-elimination for provability logic resolved. In C. Areces and R. Goldblatt, editors, Advances in Modal Logic, Vol 7, pp. 67–86. College Publications, London, 2008.Google Scholar
  10. 62.
    G. E. Hughes and M. J. Cresswell. A New Introduction to Modal Logic. Routledge, London-New York, 1996.CrossRefGoogle Scholar
  11. 72.
    S. Kripke. Semantical analysis of modal logic I: Normal modal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 11:3–16, 1968.CrossRefGoogle Scholar
  12. 74.
    D. Leivant. On the proof theory of the modal logic for arithmetic provability. Journal of Symbolic Logic, 46:531–538, 1981.CrossRefGoogle Scholar
  13. 75.
    E. Lemmon and D. Scott. An Introduction to Modal Logic. Blackwell, Oxford, 1977.Google Scholar
  14. 79.
    G. Mints. Cut-free calculi of the S5 type. Studies in constructive mathematics and mathematical logic. Part II. Seminars in Mathematics, 8:79–82, 1970.Google Scholar
  15. 80.
    G. Mints. Gentzen-type systems and resolution rules. Part I. Propositional logic. In P. Martin-Löf and G. Mints, editors, COLOG-88 Lecture Notes in Computer Science 417, pp. 198–231. Springer, Berlin, 1990.Google Scholar
  16. 81.
    G. Mints. A Short Introduction to Modal Logic. CSLI Publications, Stanford, 1992.Google Scholar
  17. 83.
    A. Moen. The proposed algorithms for eliminating cuts in the provability calculus GLS do not terminate. NWPT 2001, Norwegian Computing Center, 2001-12-10, 2001.Google Scholar
  18. 89.
    M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi. Osaka Mathematical Journal, 9:113–130, 1957.Google Scholar
  19. 90.
    M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi II. Osaka Mathematical Journal, 11:115–120, 1959.Google Scholar
  20. 112.
    W. Rautenberg. Modal tableau calculi and interpolation. Journal of Philosophical Logic, 12:403–423, 1983.CrossRefGoogle Scholar
  21. 119.
    H. Sahlqvist. Completeness and correspondence in first and second order semantics for modal logic. In S. Kanger, editor, Proceedings of the Third Scandanavian Logic Symposium, pp. 110–143. North Holland, Amsterdam, 1975.CrossRefGoogle Scholar
  22. 121.
    G. Sambin and S. Valentini. The modal logic of provability. The sequential approach. Journal of Philosophical Logic, 11:311–342, 1982.CrossRefGoogle Scholar
  23. 122.
    K. Sasaki. Löb’s axiom and cut-elimination theorem. Journal of the Nanzan Academic Society Mathematical Sciences and Information Engineering, 1:91–98, 2001.Google Scholar
  24. 124.
    M. Sato. A cut-free Gentzen-type system for the modal logic S5. Journal of Symbolic Logic, 45:67–84, 1980.CrossRefGoogle Scholar
  25. 129.
    G. Shvarts. Gentzen style systems for K45 and K45D. In A. Meyer and M. Taitslin, editors, Logic at Botik ’89, Lectures Notes in Computer Science 363, pp. 245–256. Springer, Berlin, 1989.Google Scholar
  26. 135.
    M. Takano. Subformula property as a substitute for cut-elimination in modal propositional logics. Mathematica Japonica, 37:1129–1145, 1992.Google Scholar
  27. 138.
    S.K. Thomason. An incompleteness theorem in modal logic. Theoria, 40:150–158, 1974.Google Scholar
  28. 140.
    S. Valentini. The modal logic of provability: Cut-elimination. Journal of Philosophical Logic, 12:471–476, 1983.CrossRefGoogle Scholar
  29. 150.
    J.J. Zeman. Modal logic. The Lewis-Modal Systems. Oxford University Press, Oxford, 1973.Google Scholar
  30. 12.
    S. Blamey and L. Humberstone. A perspective on modal sequent logic. Publications of the Research Institute for Mathematical Sciences, Kyoto University, 27:763–782, 1991.CrossRefGoogle Scholar
  31. 149.
    H. Wansing. Sequent systems for modal logics. In Handbook of Philosophical Logic, Vol 8, pp. 61–145. Kluwer, Dordrecht, 2002.Google Scholar
  32. 63.
    A. Indrezejczak. Generalised sequent calculus for propositional modal logics. Logica Trianguli, 1:15–31, 1997.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations


Personalised recommendations