Abstract
In this paper, we introduce hypersequent calculi for some modal logics extending S4 modal logic. In particular, we uniformly characterize hypersequent calculi for S4, S4.2, S4.3, S5 in terms of what are called “external modal structural rules” for hypersequent calculi. In addition to the monomodal logics, we also introduce simple bimodal logics combing S4 modality with another modality from each of the rest of logics. Using a proof-theoretic method, we prove cut-elimination for the hypersequent calculi for these logics and, as applications of it, we show soundness and faithfulness of Gödel embedding for the monomodal logics and the bimodal logic combining S4 and S5.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
\(\Diamond \Box A \rightarrow \Box \Diamond A\) if we use \(\Diamond \) in the language, but we do not consider \(\Diamond \) in this paper.
- 3.
This way of combining logics is not a product or a fibring, which is known in the literature of modal logic. It is close to fusion, but with an additional combining axiom. The author does not know how to call it (since apparently there is no established technical term for this case), but thanks for an anonymous referee who suggested him to clarify this.
- 4.
For this axiom, see [8].
- 5.
This is not an arbitrary choice. Apparently, there is no meaningful way of defining embedding into formulas by using \(\Box \). The problem consists in \(R\boxdot \). (Note that \(\nvdash \Box A \rightarrow \Box \boxdot A\), which we need in order to prove soundness of the rule w.r.t. Hilbert-style system under the translation using \(\Box \).) Also, note that S4.2 + S4.2, S4.3 + S4.3, S5 + S5 have a problem even if we use \(\boxdot \) for a translation into the object language. Proving soundness w.r.t. the Hilbert-style system for e.g., S4.2 + S5, apparently requires \(\Box A \rightarrow \boxdot \Box A\), but this is not provable in the system, which can be checked by an easy model-theoretic argument.
- 6.
See [3] for some problem raised to another method of avoiding this problem.
- 7.
Case 1. The last rule is applied on only side sequents \(G\). Case 2. The last rule is any non-modal rule that does not have \(A\) as the principal formula. Case 3. The last inference is an application of non-modal left introduction rule whose principal formula is \(A\).
- 8.
Note that L\(\rightarrow \) is the only rule that lowers the number of formulas on the succedent in a cut-free proof, except contraction, since we use only context-sharing rules for \(\wedge \) and \(\vee \).
- 9.
References
Metcalfe, G., Ciabattoni, A., Montagna, F.: Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions. Fuzzy Sets Syst. 161(3), 369–389 (2010)
Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Proceedings of Logic Colloquium, Logic: From Foundations to Applications, Keele, UK, 1993, pp. 1–32. Oxford University Press, New York (1996)
Baaz, M., Ciabattoni, A., Fermüller, C.G.: Hypersequent calculi for Gödel logics - a survey. J. Logic Comput. 13, 1–27 (2003)
K. Brünnler. Nested sequents (habilitationsschrift) (2010)
Ciabattoni, A., Gabbay, D.M., Olivetti, N.: Cut-free proof systems for logics of weak excluded middle. Soft Comput. 2(4), 147–156 (1998)
Došen, K.: Logical constants as punctuation marks. Notre Dame J. Formal Logic 30(3), 362–381 (1989)
Došen, K.: Modal translations in substructural logics. J. Philos. Logic 21(3), 283–336 (1992)
Fitting, M.: Logics with several modal operators. Theoria 35, 259–266 (1969)
Fitting, M.: Proof Methods for Modal and Intuitionistic Logic. Reidel Publishing Company, Dordrecht (1983)
Goranko, V., Passy, S.: Using the universal modality: gain and questions. J. Logic Comput. 2(1), 5–30 (1992)
Indrzejczak, A.: Cut-free hypersequent calculus for S4.3. Bull. Sect. Logic 41(1), 89–104 (2012)
Kracht, M.: Power and weakness of the modal display calculus. Proof Theory of Modal Logic, pp. 93–121. Kluwer Academic Publishers, Dordrecht (1996)
Kurokawa, H.: Hypersequent calculi for intuitionistic logic with classical atoms. Ann. Pure Appl. Logic 161(3), 427–446 (2009)
Lahav, O.: From frame properties to hypersequent rules in modal logics. In: LICS, pp. 408–417 (2013)
Maehara, S.: Eine darstellung der intuitionistischen logik in der klassischen. Nagoya Math. J. 7, 45–64 (1954)
Mints, G.: Cut elimination for S4C: a case study. Stud. Logica. 82(1), 121–132 (2006)
Negri, N.: Proof analysis in modal logic. J. Philos. Logic 34(5–6), 507–544 (2005)
Paoli, F.: Quine and Slater on paraconsistency and deviance. J. Philos. Logic 32(2), 531–548 (2003)
Sambin, G., Battilotti, G., Faggian, C.: Basic logic: reflection, symmetry, visibility. J. Symbolic Logic 65(3), 979–1013 (2000)
Shvarts, G.F.: Gentzen style systems for K45 and K45D. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik ’89. LNCS, vol. 363, pp. 245–256. Springer, Heidelberg (1989)
Wansing, H.: Displaying Modal Logic. Kluwer Academic Publishers, Dordrecht (1998)
Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 8, 2nd edn, pp. 61–146. Kluwer Academic Publishers, Amsterdam (2002)
Zeman, J.J.: Modal Logic/The Lewis-Modal System, 1st edn. Oxford University Press, Oxford (1973)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Kurokawa, H. (2014). Hypersequent Calculi for Modal Logics Extending S4. In: Nakano, Y., Satoh, K., Bekki, D. (eds) New Frontiers in Artificial Intelligence. JSAI-isAI 2013. Lecture Notes in Computer Science(), vol 8417. Springer, Cham. https://doi.org/10.1007/978-3-319-10061-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-10061-6_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10060-9
Online ISBN: 978-3-319-10061-6
eBook Packages: Computer ScienceComputer Science (R0)