Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames.
Saved in:
| Title: | Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames. |
|---|---|
| Authors: | Rybakov, Mikhail1 (AUTHOR), Shkatov, Dmitry2 (AUTHOR) |
| Source: | Journal of Logic & Computation. Mar2025, Vol. 35 Issue 2, p1-27. 27p. |
| Subjects: | Predicate (Logic), Proposition (Logic), Modal logic, Logic |
| Abstract: | We show that the monadic fragment of the modal predicate logic of a single Kripke frame with finitely many possible worlds, but possibly infinite domains, is decidable. This holds true even for multimodal logics with equality, regardless of whether equality is interpreted as identity or as congruence. By the Gödel–Tarski translation, similar results follow for superintuitionistic predicate logics, with or without equality. Using these observations, we establish upper algorithmic bounds, which match the known lower bounds, for monadic fragments of some modal predicate logics. In particular, we prove that, if |$L$| is a propositional modal logic contained in |$\textbf{S5}$| , |$\textbf{GL.3}$| or |$\textbf{Grz.3}$| and the class of finite Kripke frames validating |$L$| is recursively enumerable, then the monadic fragment with equality of the predicate logic of finite Kripke frames validating |$L$| is |$\varPi ^{0}_{1}$| -complete; this, in particular, holds if |$L$| is one of the following propositional logics: |$\textbf{K}$| , |$\textbf{T}$| , |$\textbf{D}$| , |$\textbf{KB}$| , |$\textbf{KTB}$| , |$\textbf{K4}$| , |$\textbf{K4.3}$| , |$\textbf{S4}$| , |$\textbf{S4.3}$| , |$\textbf{GL}$| , |$\textbf{Grz}$| , |$\textbf{K5}$| , |$\textbf{K45}$| and |$\textbf{S5}$|. We also prove that monadic fragments with equality of logics |$\textbf{QAlt}^=_{n}$| and |$\textbf{QTAlt}^=_{n}$| are decidable. The obtained results are easily extendable to the multimodal versions of the predicate logics we consider and to logics with the Barcan formula. [ABSTRACT FROM AUTHOR] |
| Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
|
Full text is not displayed to guests.
Login for full access.
|
|
| Abstract: | We show that the monadic fragment of the modal predicate logic of a single Kripke frame with finitely many possible worlds, but possibly infinite domains, is decidable. This holds true even for multimodal logics with equality, regardless of whether equality is interpreted as identity or as congruence. By the Gödel–Tarski translation, similar results follow for superintuitionistic predicate logics, with or without equality. Using these observations, we establish upper algorithmic bounds, which match the known lower bounds, for monadic fragments of some modal predicate logics. In particular, we prove that, if |$L$| is a propositional modal logic contained in |$\textbf{S5}$| , |$\textbf{GL.3}$| or |$\textbf{Grz.3}$| and the class of finite Kripke frames validating |$L$| is recursively enumerable, then the monadic fragment with equality of the predicate logic of finite Kripke frames validating |$L$| is |$\varPi ^{0}_{1}$| -complete; this, in particular, holds if |$L$| is one of the following propositional logics: |$\textbf{K}$| , |$\textbf{T}$| , |$\textbf{D}$| , |$\textbf{KB}$| , |$\textbf{KTB}$| , |$\textbf{K4}$| , |$\textbf{K4.3}$| , |$\textbf{S4}$| , |$\textbf{S4.3}$| , |$\textbf{GL}$| , |$\textbf{Grz}$| , |$\textbf{K5}$| , |$\textbf{K45}$| and |$\textbf{S5}$|. We also prove that monadic fragments with equality of logics |$\textbf{QAlt}^=_{n}$| and |$\textbf{QTAlt}^=_{n}$| are decidable. The obtained results are easily extendable to the multimodal versions of the predicate logics we consider and to logics with the Barcan formula. [ABSTRACT FROM AUTHOR] |
|---|---|
| ISSN: | 0955792X |
| DOI: | 10.1093/logcom/exad078 |
