An extension of Kracht's theorem to generalized Sahlqvist formulas

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.