# Sahlqvist theorem

To be precise, let a positive (negative) formula of modal logic be one where all proposition letters occur in the scope of an even (odd) number of negation signs only. Let a Sahlqvist antecedent be a formula that is built up from proposition letters prefixed by any finite number of necessity operators $\Box$ and negative formulas, using only $\lor$, $\land$ and the possibility operator $\Diamond$. Then, a Sahlqvist formula is any formula that may be obtained by applying conjunctions and necessity operators $\Box$ to implications of the form $\phi\to\psi$, where $\phi$ is a Sahlqvist antecedent and $\psi$ is a positive formula. For example, $\alpha=\Diamond\Box p\to\Box p$ is a Sahlqvist formula.
Sahlqvist's theorem states two things. First, although, in general, every modal formula is equivalent to a second-order formula, Sahlqvist formulas have a first-order equivalent (cf. Modal logic); moreover, this first-order equivalent $FO(\varphi)$ of $\varphi$ may be obtained in an effective way. For instance, for $\alpha$ as above, $FO(\alpha)$ expresses Euclidicity: $\forall x\forall y\forall z((Rxy\land Rxz)\to Ryz)$. Secondly, every Sahlqvist formula is canonical. Here, canonicity of a modal formula means that it is valid on the canonical frame. Algebraically, the latter may be viewed as the Stone representation of the free Boolean algebra with operators over $\omega$ many generators. Canonicity of a modal formula $\varphi$ implies that the modal logic obtained from the minimal logic $K$ by adding $\varphi$ as an axiom, is axiomatically complete with respect to the class of models satisfying $FO(\varphi)$. Thus, the modal logic $K+\alpha$ is complete with respect to Euclidean Kripke frames (cf. also Kripke models).