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. enter image description here


1 Answer 1


There exist two definitions of consequence in modal logic:

  • local validity: Truth is preserved on a per-world level; this is the definition you are proposing.

  • 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$)).

The local definition is the one that is probably the more convincing one intuitively.

  • $\begingroup$ Thanks! Though I do wonder why clear formulations of this foundational definition are so hard to find... It is very dangerous to simply use natural language in such a complex case. $\endgroup$
    – God bless
    Jan 22, 2023 at 21:26
  • $\begingroup$ There is extensive research on modal consequence relations. But since most modal logic textbooks have nowadays have strong computational affinities, you won't find much of the material there. For a start, you might have a look at the chapter on the topic contained in the Handbook of Modal Logic. But the author is Marcus Kracht and so you're in for some difficult mathematics (at least by my lights). wwwhomes.uni-bielefeld.de/mkracht/html/themes.pdf $\endgroup$
    – sequitur
    Jan 23, 2023 at 22:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .