Document Open Access Logo

Bundled Fragments of First-Order Modal Logic: (Un)Decidability

Authors Anantha Padmanabha , R Ramanujam, Yanjing Wang

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.43.pdf
  • Filesize: 0.6 MB
  • 20 pages

Document Identifiers

Author Details

Anantha Padmanabha
  • Institute of Mathematical Sciences, HBNI, Chennai, India
R Ramanujam
  • Institute of Mathematical Sciences, HBNI, Chennai, India
Yanjing Wang
  • Department of Philosophy, Peking University, Beijing, China

Cite As Get BibTex

Anantha Padmanabha, R Ramanujam, and Yanjing Wang. Bundled Fragments of First-Order Modal Logic: (Un)Decidability. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 43:1-43:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2018.43

Abstract

Quantified modal logic is notorious for being undecidable, with very few known decidable fragments such as the monodic ones. For instance, even the two-variable fragment over unary predicates is undecidable. In this paper, we study a particular fragment, namely the bundled fragment, where a first-order quantifier is always followed by a modality when occurring in the formula, inspired by the proposal of [Yanjing Wang, 2017] in the context of non-standard epistemic logics of know-what, know-how, know-why, and so on.
As always with quantified modal logics, it makes a significant difference whether the domain stays the same across possible worlds. In particular, we show that the predicate logic with the bundle "forall Box" alone is undecidable over constant domain interpretations, even with only monadic predicates, whereas having the "exists Box" bundle instead gives us a decidable logic. On the other hand, over increasing domain interpretations, we get decidability with both "forall Box" and "exists Box" bundles with unrestricted predicates, where we obtain tableau based procedures that run in PSPACE. We further show that the "exists Box" bundle cannot distinguish between constant domain and variable domain interpretations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • First-order modal logic
  • decidability
  • bundled fragments

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Logic in Computer Science, 1996. LICS'96. Proceedings., Eleventh Annual IEEE Symposium on, pages 313-321. IEEE, 1996. Google Scholar
  2. Francesco Belardinelli and Alessio Lomuscio. Interactions between knowledge and time in a first-order logic for multi-agent systems: completeness results. Journal of Artificial Intelligence Research, 45:1-45, 2012. Google Scholar
  3. Egon Börger, Erich Grädel, and Yuri Gurevich. The classical decision problem. Springer Science &Business Media, 2001. Google Scholar
  4. Gisèle Fischer-Servi et al. The finite model property for MIPQ and some consequences. Notre Dame Journal of Formal Logic, 19(4):687-692, 1978. Google Scholar
  5. Melvin. Fitting and Richard L Mendelsohn. First-order modal logic. Synthese Library. Springer, 1998. Google Scholar
  6. D. M. Gabbay and V. B. Shehtman. Undecidability of Modal and Intermediate First-Order Logics with Two Individual Variables. J. Symbolic Logic, 58(3):800-823, September 1993. URL: https://projecteuclid.org:443/euclid.jsl/1183744299.
  7. Kurt Gödel. Zum entscheidungsproblem des logischen funktionenkalküls. Monatshefte für Mathematik und Physik, 40(1):433-443, 1933. Google Scholar
  8. G. E. Hughes and M. J. Cresswell. A New Introduction to Modal Logic. Routledge, 1996. Google Scholar
  9. Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev. Undecidability of first-order intuitionistic and modal logics with two variables. Bull. Symbolic Logic, 11(3):428-438, September 2005. URL: http://dx.doi.org/10.2178/bsl/1122038996.
  10. Saul A. Kripke. The Undecidability of Monadic Modal Quantification Theory. Mathematical Logic Quarterly, 8(2):113-116, 1962. URL: http://dx.doi.org/10.1002/malq.19620080204.
  11. Mikhail N. Rybakov and Dmitry Shkatov. Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter. CoRR, abs/1706.05060, 2017. URL: http://arxiv.org/abs/1706.05060.
  12. Krister Segerberg. Two-Dimensional Modal Logic. Journal of Philosophical Logic, 2(1):77-96, 1973. URL: http://www.jstor.org/stable/30226970.
  13. Moshe Y Vardi. Why is modal logic so robustly decidable? Technical report, Rice University, 1997. Google Scholar
  14. Yanjing Wang. A logic of goal-directed knowing how. Synthese, 2017. forthcoming. Google Scholar
  15. Yanjing Wang. A New Modal Framework for Epistemic Logic. In Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2017, Liverpool, UK, 24-26 July 2017., pages 515-534, 2017. URL: http://dx.doi.org/10.4204/EPTCS.251.38.
  16. Yanjing Wang. Beyond knowing that: a new generation of epistemic logics. In Jaakko Hintikka on knowledge and game theoretical semantics, pages 499-533. Springer, 2018. Google Scholar
  17. Frank Wolter and Michael Zakharyaschev. Decidable Fragments of First-Order Modal Logics. The Journal of Symbolic Logic, 66(3):1415-1438, 2001. URL: http://www.jstor.org/stable/2695115.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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