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.
Keywords
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.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
- 2.
In fact other kinds of components, for example expressing clusters, were also proposed recently, see e.g. Baelde, Lick and Schmitz [6].
- 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
Avron, A.: A constructive analysis of RM. J. Symb. Log. 52, 939–951 (1987)
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)
Avron, A., Honsell, F., Miculan, M., Paravano, C.: Encoding modal logics in logical frameworks. Stud. Log. 60, 161–202 (1998)
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)
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)
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)
Bednarska, K., Indrzejczak, A.: Hypersequent calculi for S5 - the methods of cut-elimination. Log. Log. Philos. 24(3), 277–311 (2015)
Blamey, S., Humberstone, L.: A perspective on modal sequent logic. Publications of the Research Institute for Mathematical Sciences, Kyoto University 27, 763–782 (1991)
Braüner, T.: Hybrid Logic and its Proof-Theory. Springer, Roskilde (2009). https://doi.org/10.1007/978-94-007-0002-4
Brünnler, K.: Deep sequent systems for modal logic. Arch. Math. Log. 48(6), 551–571 (2009)
Bull, R.A.: Cut elimination for propositional dynamic logic without star. Z. für Math. Log. Und Grundl. Math. 38, 85–100 (1992)
Ciabattoni, A., Ramanayake, R., Wansing, H.: Hypersequent and display calculi - a unified perspective. Stud. Log. 102(6), 1245–1294 (2014)
Curry, H.B.: A Theory of Formal Deducibility. University of Notre Dame Press, Notre Dame (1950)
Dos̆en, K.: Sequent-systems for modal logic. J. Symb. Log. 50, 149–159 (1985)
Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht (1983)
Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Log. 163, 291–313 (2012)
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)
Girard, J.Y.: Proof Theory and Logical Complexity. Bibliopolis, Napoli (1987)
Hähnle, R.: Automated Deduction in Multiple-Valued Logics. Oxford University Press, Oxford (1994)
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
Indrzejczak, A.: Cut-free double sequent calculus for S5. Log. J. IGPL 6(3), 505–516 (1998)
Indrzejczak, A.: Generalised sequent calculus for propositional modal logics. Log. Trianguli 1, 15–31 (1997)
Indrzejczak, A.: Multiple Sequent Calculus for Tense Logics. Abstracts of AiML and ICTL 2000, Leipzig, pp. 93–104 (2000)
Indrzejczak, A.: Natural Deduction, Hybrid Systems and Modal Logics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-90-481-8785-0
Indrzejczak, A.: Simple decision procedure for S5 in standard cut-free sequent calculus. Bull. Sect. Log. 45(2), 125–140 (2016)
Indrzejczak, A.: Linear time in hypersequent framework. Bull. Symb. Log. 22(1), 121–144 (2016)
Kashima, R.: Cut-free sequent calculi for some tense logics. Stud. Log. 53, 119–135 (1994)
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
Lahav O.: From frame properties to hypersequent rules in modal logics. In: Proceedings of LICS, pp. 408–417. Springer (2013)
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
Metcalfe, G., Olivetti, N., Gabbay, D.: Proof Theory for Fuzzy Logics. Springer, Heidelberg (2008). https://doi.org/10.1007/978-1-4020-9409-5
Mints, G.: Some calculi of modal logic [in Russian]. Trudy Mat. Inst. Steklov. 98, 88–111 (1968)
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)
Mints, G.: Selected Papers in Proof Theory. North-Holland, Amsterdam (1992)
Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)
Negri, S.: Proof analysis in modal logic. J. Philos. Log. 34, 507–544 (2005)
Ohnishi, M., Matsumoto, K.: Gentzen method in modal calculi I. Osaka Math. J. 9, 113–130 (1957)
Poggiolesi, F.: Gentzen Calculi for Modal Propositional Logic. Springer, Heidelberg (2011)
Pottinger, G.: Uniform cut-free formulations of T, S4 and S5 (abstract). J. Symb. Log. 48, 900 (1983)
Restall, G.: Proofnets for S5: sequents and circuits for modal logic. Lect. Notes Log. 28, 151–172 (2007)
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)
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)
Stouppa, P.: A deep inference system for the modal logic S5. Stud. Log. 85, 199–214 (2007)
Wansing, H.: Displaying Modal Logics. Kluwer Academic Publishers, Dordrecht (1999)
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)
Zeman, J.: Modal Logic. Oxford University Press, Oxford (1973)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)