Skip to main content
SpringerLink
Log in
Book cover

JSAI International Symposium on Artificial Intelligence

JSAI-isAI 2013: New Frontiers in Artificial Intelligence pp 51–68Cite as

Hypersequent Calculi for Modal Logics Extending S4

  • Conference paper
  • First Online:

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

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Notes

  1. 1.

    However, see [2] for critical discussions about display calculi. Also, there exist sequent calculi for these logics, but the one for S4.2 is not cut-free [23], and the one for S4.3 does not satisfy one of the desiderata for good proof systems in [2].

  2. 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. 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. 4.

    For this axiom, see [8].

  5. 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. 6.

    See [3] for some problem raised to another method of avoiding this problem.

  7. 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. 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. 9.

    This turns out to be a hypersequent variant of the arguments in [15] and [7].

References

  1. 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)

    Article  MathSciNet  Google Scholar 

  2. 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)

    Google Scholar 

  3. Baaz, M., Ciabattoni, A., Fermüller, C.G.: Hypersequent calculi for Gödel logics - a survey. J. Logic Comput. 13, 1–27 (2003)

    Article  Google Scholar 

  4. K. Brünnler. Nested sequents (habilitationsschrift) (2010)

    Google Scholar 

  5. Ciabattoni, A., Gabbay, D.M., Olivetti, N.: Cut-free proof systems for logics of weak excluded middle. Soft Comput. 2(4), 147–156 (1998)

    Article  Google Scholar 

  6. Došen, K.: Logical constants as punctuation marks. Notre Dame J. Formal Logic 30(3), 362–381 (1989)

    Article  MathSciNet  Google Scholar 

  7. Došen, K.: Modal translations in substructural logics. J. Philos. Logic 21(3), 283–336 (1992)

    Article  MathSciNet  Google Scholar 

  8. Fitting, M.: Logics with several modal operators. Theoria 35, 259–266 (1969)

    Article  MathSciNet  Google Scholar 

  9. Fitting, M.: Proof Methods for Modal and Intuitionistic Logic. Reidel Publishing Company, Dordrecht (1983)

    Book  Google Scholar 

  10. Goranko, V., Passy, S.: Using the universal modality: gain and questions. J. Logic Comput. 2(1), 5–30 (1992)

    Article  MathSciNet  Google Scholar 

  11. Indrzejczak, A.: Cut-free hypersequent calculus for S4.3. Bull. Sect. Logic 41(1), 89–104 (2012)

    MathSciNet  MATH  Google Scholar 

  12. Kracht, M.: Power and weakness of the modal display calculus. Proof Theory of Modal Logic, pp. 93–121. Kluwer Academic Publishers, Dordrecht (1996)

    Chapter  Google Scholar 

  13. Kurokawa, H.: Hypersequent calculi for intuitionistic logic with classical atoms. Ann. Pure Appl. Logic 161(3), 427–446 (2009)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  15. Maehara, S.: Eine darstellung der intuitionistischen logik in der klassischen. Nagoya Math. J. 7, 45–64 (1954)

    Article  MathSciNet  Google Scholar 

  16. Mints, G.: Cut elimination for S4C: a case study. Stud. Logica. 82(1), 121–132 (2006)

    Article  MathSciNet  Google Scholar 

  17. Negri, N.: Proof analysis in modal logic. J. Philos. Logic 34(5–6), 507–544 (2005)

    Article  MathSciNet  Google Scholar 

  18. Paoli, F.: Quine and Slater on paraconsistency and deviance. J. Philos. Logic 32(2), 531–548 (2003)

    Article  MathSciNet  Google Scholar 

  19. Sambin, G., Battilotti, G., Faggian, C.: Basic logic: reflection, symmetry, visibility. J. Symbolic Logic 65(3), 979–1013 (2000)

    Article  MathSciNet  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Wansing, H.: Displaying Modal Logic. Kluwer Academic Publishers, Dordrecht (1998)

    Book  Google Scholar 

  22. 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)

    Chapter  Google Scholar 

  23. Zeman, J.J.: Modal Logic/The Lewis-Modal System, 1st edn. Oxford University Press, Oxford (1973)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information Science, Kobe University, Kobe, Japan

    Hidenori Kurokawa

Authors
  1. Hidenori Kurokawa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hidenori Kurokawa .

Editor information

Editors and Affiliations

  1. Seikei University, Musashino-shi, Tokyo, Japan

    Yukiko Nakano

  2. National Institute of Informatics Research Division, Tokyo, Japan

    Ken Satoh

  3. Ochanomizu University, Tokyo, Japan

    Daisuke Bekki

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation