Sahlqvist formulas are a syntactically specified class of modal formulas proposed by Hendrik Sahlqvist in 1975. They are important because of their first-order definability and canonicity, and hence axiomatize complete modal logics. The first-order properties definable by Sahlqvist formulas were syntactically characterized by Marcus Kracht in 1993. The present paper extends Kracht's theorem to the class of ‘generalized Sahlqvist formulas' introduced by Goranko and Vakarelov and describes an appropriate generalization of Kracht formulas.

We characterize the modal logics of elementary classes of Kripke frames as precisely those modal logics that are axiomatized by modal axioms synthesized in a certain effective way from "quasi-positive" sentences of hybrid logic. These are pure positive hybrid sentences with arbitrary existential and relativized universal quantification over nominals. The proof has three steps. The first step is to use the known result that the modal logic of any elementary class of Kripke frames is also the modal logic of the (...) closure of this class under disjoint unions, generated subframes, bounded morphic images, and ultraroots. This latter class can be defined by the first-order sentences of a special syntactic form (called pseudo-equations by Goldblatt) that are valid in the former class. The second step is to translate these pseudo-equations into equivalent quasi-positive hybrid sentences. In the third and main step, we show that any quasi-positive sentence S generates an infinite set of modal formulas called "approximants," which together axiomatize a canonical modal logic that is sound and complete for the class of frames validating S. The proof is analogous to standard proofs of Sahlqvist's theorem. It generalizes to sets of quasi-positive sentences. The main result now follows. (shrink)

We prove that everyn-modal logic betweenKnandS5nis undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the representation problem of finite relation (...) algebras. (shrink)