2025/09/09 by Alessandro Artale, Artale, Alessandro, Christopher Hampson +7
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2509.08165
openalex publication_date 2025/09/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
While modal extensions of decidable fragments of first-order logic are usually undecidable, their monodic counterparts, in which formulas in the scope of modal operators have at most one free variable, are typically decidable. This only holds, however, under the provision that non-rigid constants, definite descriptions and non-trivial counting are not admitted. Indeed, several monodic fragments having at least one of these features are known to be undecidable. We investigate these features systematically and show that fundamental monodic fragments such as the two-variable fragment with counting and the guarded fragment of standard first-order modal logics Kn and S5n are decidable. Tight complexity bounds are established as well. Under the expanding-domain semantics, we show decidability of the basic modal logic extended with the transitive closure operator on finite acyclic frames; this logic, however, is Ackermann-hard.