Document Open Access Logo

A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus

Authors Philippe Balbiani , Han Gao , Çiğdem Gencer , Nicola Olivetti

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2024.13.pdf
  • Filesize: 0.94 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Proof theory
Keywords
  • Intuitionistic Modal Logic
  • Axiomatization
  • Completeness
  • Sequent Calculus

Metrics

Abstract

We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it directly.

Cite As Get BibTex

Philippe Balbiani, Han Gao, Çiğdem Gencer, and Nicola Olivetti. A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.13

Author Details

Philippe Balbiani
  • CNRS-INPT-UT3, IRIT, Toulouse, France
Han Gao
  • Aix-Marseille University, CNRS, LIS, Marseille, France
Çiğdem Gencer
  • CNRS-INPT-UT3, IRIT, Toulouse, France
Nicola Olivetti
  • Aix-Marseille University, CNRS, LIS, Marseille, France

Acknowledgements

This paper is originated from a discussion started by Anupam Das and Sonia Marin in the proof theory blog (see the link https://prooftheory.blog/2022/08/19/), we are grateful to them as well as all other contributors to the discussion. In particular, Example 24 was reported in the blog by Alex Simpson, who learnt it in 1996 by Carsten Grefe in a private communication. Example 55 was suggested first by Anupam Das and Sonia Marin in the blog. Finally we thank the reviewers for their very helpful criticisms and insightful remarks.

References

  1. Philippe Balbiani, Martín Diéguez, and David Fernández-Duque. Some constructive variants of S4 with the finite model property. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470643.
  2. Gianluigi Bellin, Valeria De Paiva, and Eike Ritter. Extended curry-howard correspondence for a basic constructive modal logic. In Proceedings of methods for modalities, volume 2, 2001. Google Scholar
  3. Kai Brünnler. Deep sequent systems for modal logic. Arch. Math. Log., 48(6):551-577, 2009. URL: https://doi.org/10.1007/S00153-009-0137-3.
  4. Anupam Das and Sonia Marin. On intuitionistic diamonds (and lack thereof). In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, volume 14278 of Lecture Notes in Computer Science, pages 283-301. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43513-3_16.
  5. Frederic B. Fitch. Intuitionistic modal logic with quantifiers. Portugaliae mathematica, 7(2):113-118, 1948. URL: http://eudml.org/doc/114664.
  6. Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame J. Formal Log., 55(1):41-61, 2014. URL: https://doi.org/10.1215/00294527-2377869.
  7. Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz Straßburger. Intuitionistic S4 is decidable. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175684.
  8. Tim S. Lyon. Nested sequents for intuitionistic modal logics via structural refinement. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, volume 12842 of Lecture Notes in Computer Science, pages 409-427. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86059-2_24.
  9. Sonia Marin and Marianela Morales. Fully structured proof theory for intuitionistic modal logics. In AiML 2020 - Advances in Modal Logic, 2020. URL: https://hal.science/hal-03048959.
  10. Sonia Marin, Marianela Morales, and Lutz Straßburger. A fully labelled proof system for intuitionistic modal logics. J. Log. Comput., 31(3):998-1022, 2021. URL: https://doi.org/10.1093/LOGCOM/EXAB020.
  11. Gordon Plotkin and Colin Stirling. A framework for intuitionistic modal logics. In Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pages 399-406, 1986. URL: https://doi.org/10.5555/1029786.1029823.
  12. Dag Prawitz. Natural Deduction: A Proof-Theoretical Study. Dover Publications, Mineola, N.Y., 1965. URL: https://doi.org/10.2307/2271676.
  13. Gisèle Fischer Servi. On modal logic with an intuitionistic base. Studia Logica, 36(3):141-149, 1977. URL: https://doi.org/10.1007/BF02121259.
  14. Gisèle Fischer Servi. Semantics for a Class of Intuitionistic Modal Calculi, pages 59-72. Springer Netherlands, Dordrecht, 1981. URL: https://doi.org/10.1007/978-94-009-8937-5_5.
  15. Gisèle Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico Università e Politecnico di Torino, 42, 1984. URL: https://cir.nii.ac.jp/crid/1371132818982119684.
  16. Alex K. Simpson. The proof theory and semantics of intuitionistic modal logic. Ph.D. Thesis, University of Edinburgh, 1994. URL: https://api.semanticscholar.org/CorpusID:2309858.
  17. Duminda Wijesekera. Constructive modal logics I. Ann. Pure Appl. Log., 50(3):271-301, 1990. URL: https://doi.org/10.1016/0168-0072(90)90059-B.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact