Skip to main content
SpringerLink
Log in

Two Is Enough – Bisequent Calculus for S5

  • Conference paper
  • First Online:
Frontiers of Combining Systems (FroCoS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11715))

Included in the following conference series:

Abstract

We present a generalised sequent calculus based on the use of pairs of ordinary sequents called bisequents. It may be treated as the weakest kind of system in the rich family of systems operating on items being some collections of ordinary sequents. This family covers hypersequent and nested sequent calculi introduced for several non-classical logics. It seems that for many such logics, including some many-valued and modal ones, a reasonably modest generalization of standard sequents is sufficient. In this paper we provide a proof theoretic examination of S5 in the framework of bisequent calculus. Two versions of cut-free calculus are provided. The first version is more flexible for proof search but admits only indirect proof of cut elimination. The second version is syntactically more constrained but admits constructive proof of cut elimination. This result is extended to several versions of first-order S5.

The results reported in this paper are supported by the National Science Centre, Poland (grant number: DEC-2017/25/B/HS1/01268).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    For example, Fitting [16] results concerning the correspondence between prefixed tableaux and nested sequents, or Baaz, Fermüller and Zach [5] concerning n-sided sequents and labelled tableaux for many-valued logics.

  2. 2.

    In fact other kinds of components, for example expressing clusters, were also proposed recently, see e.g. Baelde, Lick and Schmitz [6].

  3. 3.

    For example, the method applied in Indrzejczak [25] and based on suitably defined downward saturation and loop check can be adapted to BSC1 as well. Moreover it yields decidability in propositional case.

References

  1. Avron, A.: A constructive analysis of RM. J. Symb. Log. 52, 939–951 (1987)

    Article  MathSciNet  Google Scholar 

  2. Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Hodges, W., et al. (eds.) Logic: From Foundations to Applications, pp. 1–32. Oxford Science Publication, Oxford (1996)

    Google Scholar 

  3. Avron, A., Honsell, F., Miculan, M., Paravano, C.: Encoding modal logics in logical frameworks. Stud. Log. 60, 161–202 (1998)

    Article  MathSciNet  Google Scholar 

  4. Avron, A., Lahav, O.: A simple cut-free system of paraconsistent logic equivalent to S5. In: Bezhanishvili, G., et al. (eds.) Advances in Modal Logic, vol. 12, pp. 29–42. College Publications (2018)

    Google Scholar 

  5. Baaz, M., Fermüller, C.G., Zach, R.: Dual systems of sequents and tableaux for many-valued logics. Technical report TUW-E185.2-BFZ, 2–92 (1992)

    Google Scholar 

  6. Baelde, D., Lick, A., Schmitz, S.: A hypersequent calculus with clusters for linear frames. In: Bezhanishvili, G., et al. (eds.) Advances in Modal Logic, vol. 12, pp. 43–62. College Publications (2018)

    Google Scholar 

  7. Bednarska, K., Indrzejczak, A.: Hypersequent calculi for S5 - the methods of cut-elimination. Log. Log. Philos. 24(3), 277–311 (2015)

    MathSciNet  MATH  Google Scholar 

  8. Blamey, S., Humberstone, L.: A perspective on modal sequent logic. Publications of the Research Institute for Mathematical Sciences, Kyoto University 27, 763–782 (1991)

    Article  MathSciNet  Google Scholar 

  9. Braüner, T.: Hybrid Logic and its Proof-Theory. Springer, Roskilde (2009). https://doi.org/10.1007/978-94-007-0002-4

    Book  MATH  Google Scholar 

  10. Brünnler, K.: Deep sequent systems for modal logic. Arch. Math. Log. 48(6), 551–571 (2009)

    Article  MathSciNet  Google Scholar 

  11. Bull, R.A.: Cut elimination for propositional dynamic logic without star. Z. für Math. Log. Und Grundl. Math. 38, 85–100 (1992)

    Article  Google Scholar 

  12. Ciabattoni, A., Ramanayake, R., Wansing, H.: Hypersequent and display calculi - a unified perspective. Stud. Log. 102(6), 1245–1294 (2014)

    Article  MathSciNet  Google Scholar 

  13. Curry, H.B.: A Theory of Formal Deducibility. University of Notre Dame Press, Notre Dame (1950)

    MATH  Google Scholar 

  14. Dos̆en, K.: Sequent-systems for modal logic. J. Symb. Log. 50, 149–159 (1985)

    Article  MathSciNet  Google Scholar 

  15. Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht (1983)

    Book  Google Scholar 

  16. Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Log. 163, 291–313 (2012)

    Article  MathSciNet  Google Scholar 

  17. Garson, J.W.: Quantification in modal logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, vol. II, pp. 249–308. Kluwer, Dordrecht (1984)

    Chapter  Google Scholar 

  18. Girard, J.Y.: Proof Theory and Logical Complexity. Bibliopolis, Napoli (1987)

    MATH  Google Scholar 

  19. Hähnle, R.: Automated Deduction in Multiple-Valued Logics. Oxford University Press, Oxford (1994)

    MATH  Google Scholar 

  20. Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 210–225. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61208-4_14

    Chapter  Google Scholar 

  21. Indrzejczak, A.: Cut-free double sequent calculus for S5. Log. J. IGPL 6(3), 505–516 (1998)

    Article  MathSciNet  Google Scholar 

  22. Indrzejczak, A.: Generalised sequent calculus for propositional modal logics. Log. Trianguli 1, 15–31 (1997)

    MathSciNet  MATH  Google Scholar 

  23. Indrzejczak, A.: Multiple Sequent Calculus for Tense Logics. Abstracts of AiML and ICTL 2000, Leipzig, pp. 93–104 (2000)

    Google Scholar 

  24. Indrzejczak, A.: Natural Deduction, Hybrid Systems and Modal Logics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-90-481-8785-0

    Book  MATH  Google Scholar 

  25. Indrzejczak, A.: Simple decision procedure for S5 in standard cut-free sequent calculus. Bull. Sect. Log. 45(2), 125–140 (2016)

    MathSciNet  MATH  Google Scholar 

  26. Indrzejczak, A.: Linear time in hypersequent framework. Bull. Symb. Log. 22(1), 121–144 (2016)

    Article  MathSciNet  Google Scholar 

  27. Kashima, R.: Cut-free sequent calculi for some tense logics. Stud. Log. 53, 119–135 (1994)

    Article  MathSciNet  Google Scholar 

  28. Kurokawa, H.: Hypersequent calculi for modal logics extending S4. In: Nakano, Y., Satoh, K., Bekki, D. (eds.) JSAI-isAI 2013. LNCS (LNAI), vol. 8417, pp. 51–68. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10061-6_4

    Chapter  Google Scholar 

  29. Lahav O.: From frame properties to hypersequent rules in modal logics. In: Proceedings of LICS, pp. 408–417. Springer (2013)

    Google Scholar 

  30. Lellmann, B.: Linear nested sequents, 2-sequents and hypersequents. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 135–150. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24312-2_10

    Chapter  MATH  Google Scholar 

  31. Metcalfe, G., Olivetti, N., Gabbay, D.: Proof Theory for Fuzzy Logics. Springer, Heidelberg (2008). https://doi.org/10.1007/978-1-4020-9409-5

    Book  MATH  Google Scholar 

  32. Mints, G.: Some calculi of modal logic [in Russian]. Trudy Mat. Inst. Steklov. 98, 88–111 (1968)

    MathSciNet  Google Scholar 

  33. Mints G.: Systems of Lewis and system T’ [in Russian], Supplement to Russian edition. In: Feys, R. (ed.) Modal Logic, Nauka, pp. 422–509 (1974)

    Google Scholar 

  34. Mints, G.: Selected Papers in Proof Theory. North-Holland, Amsterdam (1992)

    MATH  Google Scholar 

  35. Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)

    Book  Google Scholar 

  36. Negri, S.: Proof analysis in modal logic. J. Philos. Log. 34, 507–544 (2005)

    Article  MathSciNet  Google Scholar 

  37. Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi I. Osaka Math. J. 9, 113–130 (1957)

    MathSciNet  MATH  Google Scholar 

  38. Poggiolesi, F.: Gentzen Calculi for Modal Propositional Logic. Springer, Heidelberg (2011)

    Book  Google Scholar 

  39. Pottinger, G.: Uniform cut-free formulations of T, S4 and S5 (abstract). J. Symb. Log. 48, 900 (1983)

    Google Scholar 

  40. Restall, G.: Proofnets for S5: sequents and circuits for modal logic. Lect. Notes Log. 28, 151–172 (2007)

    MathSciNet  MATH  Google Scholar 

  41. Sato, M.: A study of kripke-type models for some modal logics by Gentzen’s sequential method. Publ. Res. Inst. Math. Sci. Kyoto Univ. 13, 381–468 (1977)

    Article  MathSciNet  Google Scholar 

  42. Serebriannikov, O.: Gentzen’s Hauptsatz for modal logic with quantifiers. In: Niniluoto, I., Saarinen, E. (eds.) Intensional Logic: Theory and Applications; Acta Philosophica Fennica, vol. 35, pp. 79–88 (1982)

    Google Scholar 

  43. Stouppa, P.: A deep inference system for the modal logic S5. Stud. Log. 85, 199–214 (2007)

    Article  MathSciNet  Google Scholar 

  44. Wansing, H.: Displaying Modal Logics. Kluwer Academic Publishers, Dordrecht (1999)

    MATH  Google Scholar 

  45. Wansing, H.: Sequent systems for modal logics. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. IV, pp. 89–133. Reidel Publishing Company, Dordrecht (2002)

    Google Scholar 

  46. Zeman, J.: Modal Logic. Oxford University Press, Oxford (1973)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Logic, University of Łódź, Lindleya 3/5, 90–131, Łódź, Poland

    Andrzej Indrzejczak

Authors
  1. Andrzej Indrzejczak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrzej Indrzejczak .

Editor information

Editors and Affiliations

  1. CNRS, University of Toulouse, Toulouse, France

    Andreas Herzig

  2. Middlesex University London, London, UK

    Andrei Popescu

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Indrzejczak, A. (2019). Two Is Enough – Bisequent Calculus for S5. In: Herzig, A., Popescu, A. (eds) Frontiers of Combining Systems. FroCoS 2019. Lecture Notes in Computer Science(), vol 11715. Springer, Cham. https://doi.org/10.1007/978-3-030-29007-8_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29007-8_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29006-1

  • Online ISBN: 978-3-030-29007-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation