The basic modal language extends propositional logic with two unary modal operators:

• $\Box \varphi$: "necessarily $\varphi$" (or "it is known that $\varphi$", "it is always the case that $\varphi$", etc.)
• $\Diamond \varphi$: "possibly $\varphi$" (defined as $\neg \Box \neg \varphi$)

Formulas are built by: $\varphi ::= p \mid \neg \varphi \mid (\varphi \land \psi) \mid \Box \varphi$, where $p$ ranges over propositional variables.

A Kripke frame is a pair $\mathcal{F} = (W, R)$ where $W$ is a non-empty set of worlds and $R \subseteq W \times W$ is the accessibility relation. A Kripke model $\mathcal{M} = (W, R, V)$ adds a valuation $V: \mathrm{Prop} \to \mathcal{P}(W)$ assigning to each proposition the set of worlds where it is true.

The satisfaction relation $\mathcal{M}, w \models \varphi$ is defined inductively:

• $\mathcal{M}, w \models p$ iff $w \in V(p)$
• $\mathcal{M}, w \models \neg \varphi$ iff $\mathcal{M}, w \not\models \varphi$
• $\mathcal{M}, w \models \varphi \land \psi$ iff $\mathcal{M}, w \models \varphi$ and $\mathcal{M}, w \models \psi$
• $\mathcal{M}, w \models \Box \varphi$ iff for all $v$ with $wRv$: $\mathcal{M}, v \models \varphi$
• $\mathcal{M}, w \models \Diamond \varphi$ iff there exists $v$ with $wRv$ and $\mathcal{M}, v \models \varphi$