Kripke models are interpretations of modal logic which turn out to be adequate under some basic constraints for a wide array of systems of modal logic.

Definition

A Kripke model is formed by three elements:

A set of worlds $W$

A visibility relationship between worlds $R$ . If $w R x$ , we will say that $w$ sees $x$ or that $x$ is a successor of $w$ .

A valuation function $V$ that associates pairs of worlds and sentence letters to truth values.

You can visualize Kripke worlds as a digraph in which each node is a world, and the edges represent visibility.

images of Kripke worlds

The valuation function can be extended to assign truth values to whole modal sentences. We will say that a world $w \in W$ makes a modal sentence $A$ true (notation: $M, w ⊨ A$ ) if it is assigned a truth value of true according to the following rules:

If $A$ is a sentence letter $p$ , then $M, w ⊨ p$ if $V (w, p) = ⊤$ .

If $A$ is a truth functional compound of sentences, then its value comes from the propositional calculus and the values of its components. For example, if $A = B \to C$ , then $M, w ⊨ A$ iff $M, w ⊭ B$ or $M, w ⊨ C$ .

If $A$ is of the form $□ B$ , then $M, w ⊨ □ B$ if $M, x ⊨ B$ for every successor $x$ of $w$ .

Given this way of assigning truth values to sentences, we will say the following:

$A$ is valid in a model $M$ (notation: $M ⊨ A$ ) if $M, w ⊨ A$ for every $w$ in $W$ .

$A$ is valid in a class of models if it is valid in every model of the class.

$A$ is satisfiable in a model $M$ if there exists $w \in W$ such that $M, w ⊨ A$ .

$A$ is satisfiable in a class of models if it is satisfiable in some model of the class.

Notice that a sentence $A$ is valid in a class of models iff its negation is not satisfiable.

Kripke models as semantics of modal logic

Kripke models are tightly connected to the interpretations of certain modal logics.

For example, they model well the rules of normal provability systems.

Exercise: show that Kripke models satisfy the necessitation rule of modal logic. That is, if $A$ is valid in $M$ , then $□ A$ is valid in $M$ .

Show solution

Let Invalid LaTeX $w\inW: TeX parse error: Undefined control sequence \inW be a world of $M$ . Let $x$ be an arbitrary successor of $w$ . Then, as $M ⊨ A$ , then $M, x ⊨ A$ . Since $x$ was arbitrary, every successor of $w$ models $A$ , so $w ⊨ □ A$ . As $w$ was arbitrary, then every world in $M$ models $□ A$ , and thus $M ⊨ □ A$ .

Exercise: Show that the distributive axioms are always valid in Kripke models. Distributive axioms are modal sentences of the form $□ [A \to B] \to (□ A \to □ B)$ .

Show solution

Suppose that $w \in W$ is such that $w ⊨ □ [A \to B]$ and $w ⊨ □ A$ .

Let $x$ be a successor of $w$ . Then $x ⊨ A \to B$ and $x ⊨ A$ . We conclude by the propositional calculus that $x ⊨ B$ , so as $x$ was an arbitrary successor we have that $w ⊨ □ B$ , and thus $w ⊨ □ [A \to B] \to (□ A \to □ B)$ .

We conclude that $M ⊨ □ [A \to B] \to (□ A \to □ B)$ , no matter what $M$ is.

Those two last exercises prove that the K system of modal logic is sound for the class of all Kripke models. This is because we have proved that its axioms and rules of inference hold in all Kripke models (propositional tautologies and modus ponens trivially hold).

Some adequacy theorems

Now we present a relation of modal logics and the class of Kripke models in which they are adequate. You can check the proofs of adequacy in their respective pages.

The class of all Kripke models is adequate to the K system

The class of transitive Kripke models is adequate to K4

The class of reflexive Kripke models is adequate to T

The class of reflexive and transitive Kripke models is adequate to S4

The class of reflexive and symmetric Kripke models is adequate to B

The class of reflexive and euclidean Kripke models is adequate to S5

The class of finite, irreflexive and transitive Kripke models is adequate to GL

Notice that as the constraint on the models becomes stronger, the set of valid sentences increases, and thus the correspondent adequate system is stronger.

A note about notation may be in order. We say that a Kripke model is, e.g, transitive if its visibility relation is transitive ^[1]. Similarly, a Kripke model is finite if its set of worlds is finite.

^{^︎}
Same for reflexive, symmetric and euclidean