Some characterization and preservation theorems in modal logic (Q714726)

The paper discusses the relations between modal definability of classes of Kripke models and closure of these classes with respect to various algebraic constructions, in the spirit of the work of De Rijke and Sturm. The main results are the following. Call a class \(K\) of models \(\exists\)-modally definable if there is a set \(\Sigma\) of formulas such that a model \(M\) belongs to \(K\) if and only if every formula in \(\Sigma\) is satisfiable in \(M\). Then a class \(K\) is \(\exists\)-modally definable if and only if \(K\) is closed under total bisimulations, ultraproducts and the complement of \(K\) is closed under ultrapowers. Similar characterizations are given for classes \(\exists\)-modally definable with finite sets of formulas or single formulas. A more complex notion is \(\forall\exists\)-definability. Call a class \(K\) of models \(\forall\exists\)-modally definable if there is a pair of sets of formulas \((\Sigma_1,\Sigma_2)\) such that \(M\) is in \(K\) if and only if every formula in \(\Sigma_1\) is globally true on \(M\) and every formula in \(\Sigma_2\) is satisfiable in \(M\). Then \(K\) is \(\forall\exists\)-modally definable if and only if \(K\) is closed under total surjective bisimulation, disjoint union, ultraproduct, the complement of \(K\) is closed under ultrapowers, and \(K\) is closed under generated intermodels (roughly speaking, if \(M_1,M_2\) are in \(K\), and \(M\) is between \(M_1\) and \(M_2\), then \(M\) is also in \(K\); to be precise one has to introduce the notion of generated submodel). A similar characterization is possible for pairs of finite sets of formulas. Further, \(K\) is called generalized modally definable if \(K\) is the class of all models of a set of Boolean combinations of universally quantified modal formulas, where the quantifier is intended to range over all worlds of the Kripke model. Now \(K\) is generalized modally definable if and only if \(K\) is closed under total surjective bisimulation and ultraproducts, and the complement of \(K\) is closed under ultrapowers. A similar characterizations is given for classes generalized modally definable with a single sentence. Besides these main results, we find several refinements and quite a lot of examples.