# The definition of the semantic consequence relation for modal logic

I have been unable to find a general definition of semantic consequence ($$\vDash$$) for modal logic, so I would appreciate if you commented on this speculation of mine:

Definition. Let $$M = (W, R, V)$$ be a model of modal logic and $$X$$ a set of formulas. Then, $$X \vDash \varphi :\Leftrightarrow \forall M.\forall w \in W.(\forall\psi \in X.(M\vDash_w \psi) \Rightarrow M \vDash_w \varphi).$$

Here, $$M \vDash_w \varphi$$ is the standard recursively defined satisfiability relation.

Did I get it right? Thank you for the feedback. :)

P.S. For added context, I am trying to formalize the below definition found in the SEP entry on modal logic. That is, my definition of $$\vDash$$ is really only a formalization of $$\mathbf{K}$$-validity.

• global validity: Truth is preserved at a per-model level: $$X \vDash \phi \Leftrightarrow \forall M. ((\forall \psi \in X. M \models \psi) \to M \models \phi)$$, i.e., $$\Leftrightarrow \forall M. ((\forall \psi \in X. \forall w \in W. M \models_w \psi) \to (\forall w \in W. M \models_w \phi$$)).