Satisfiability vs. Finite Satisfiability in Elementary Modal Logics

TL;DR

This paper explores the decidability of satisfiability problems in elementary modal logics, revealing that some logics have decidable satisfiability but undecidable finite satisfiability, and vice versa, highlighting fundamental differences.

Contribution

It proves the existence of universal first-order formulas that define elementary modal logics with contrasting decidability properties for satisfiability and finite satisfiability.

Findings

Existence of logics with decidable satisfiability but undecidable finite satisfiability.

Existence of logics with decidable finite satisfiability but undecidable satisfiability.

Fundamental separation between general and finite satisfiability in elementary modal logics.

Abstract

We study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for finite satisfiability [11, 12, 16, 17]. In this paper, we show that there is a reason why we must deal with both kinds of satisfiability separately -- we prove that there is a universal first-order formula that defines an elementary modal logic with decidable (global) satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.