Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames.

Saved in:
Bibliographic Details
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.
FullText Links:
  – Type: pdflink
Text:
  Availability: 1
Header DbId: egs
DbLabel: Engineering Source
An: 184348321
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Rybakov%2C+Mikhail%22">Rybakov, Mikhail</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Shkatov%2C+Dmitry%22">Shkatov, Dmitry</searchLink><relatesTo>2</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Mar2025, Vol. 35 Issue 2, p1-27. 27p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Predicate+%28Logic%29%22">Predicate (Logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Proposition+%28Logic%29%22">Proposition (Logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Modal+logic%22">Modal logic</searchLink><br /><searchLink fieldCode="DE" term="%22Logic%22">Logic</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=184348321
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1093/logcom/exad078
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 27
        StartPage: 1
    Subjects:
      – SubjectFull: Predicate (Logic)
        Type: general
      – SubjectFull: Proposition (Logic)
        Type: general
      – SubjectFull: Modal logic
        Type: general
      – SubjectFull: Logic
        Type: general
    Titles:
      – TitleFull: Algorithmic properties of modal and superintuitionistic logics of monadic predicates over finite Kripke frames.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Rybakov, Mikhail
      – PersonEntity:
          Name:
            NameFull: Shkatov, Dmitry
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 03
              Text: Mar2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 0955792X
          Numbering:
            – Type: volume
              Value: 35
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Journal of Logic & Computation
              Type: main
ResultId 1