Affiliations: University of Wrocław, Faculty of Mathematics and Computer Science, Institute of Computer Science, F. Joliot-Curie 15, 50-383 Wrocław, Poland. {jmi, jotop, pwit}@cs.uni.wroc.pl
Correspondence:
[†]
Address for correspondence: 50-383 Wrocław, F. Joliot-Curie 15, Poland.
Note: [*] This research was supported by Polish National Science Center grant No 2014/15/D/ST6/00719.
Abstract: We study variants of the satisfiability problem of elementary modal logics, i.e., modal logic considered over first-order definable classes of frames. The standard semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. A number of decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and finite satisfiability. In this paper we justify that the results for both kinds of the satisfiability problem must be shown separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable general satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal first-order formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.
