An extension of Kracht's theorem to generalized Sahlqvist formulas

TL;DR

This paper extends Kracht's theorem to generalized Sahlqvist formulas, broadening the class of modal formulas with first-order definability and canonicity, which are crucial for axiomatizing complete modal logics.

Contribution

It provides a generalization of Kracht's theorem to the class of generalized Sahlqvist formulas, enhancing understanding of their first-order properties.

Findings

Extended Kracht's theorem to generalized Sahlqvist formulas

Characterized first-order definability for a broader class of modal formulas

Provided a generalized form of Kracht formulas

Abstract

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.