Kripke model

by Jaime Sevilla Molina Jul 26 2016 updated Jul 26 2016

The semantics of modal logic

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.


A Kripke model $~$M$~$ is formed by three elements:

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

[todo: 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\models A$~$) if it is assigned a truth value of true according to the following rules:

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

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 $~$\square A$~$ is valid in $~$M$~$.

%%hidden(Show solution): Let $~$w \in W$~$ be a world of $~$M$~$. Let $~$x$~$ be an arbitrary successor of $~$w$~$. Then, as $~$M\models A$~$, then $~$M,x\models A$~$. Since $~$x$~$ was arbitrary, every successor of $~$w$~$ models $~$A$~$, so $~$w\models \square A$~$. As $~$w$~$ was arbitrary, then every world in $~$M$~$ models $~$\square A$~$, and thus $~$M\models \square A$~$. %%

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

%%hidden(Show solution): Suppose that $~$w \in W$~$ is such that $~$w\models \square[A\to B]$~$ and $~$w\models \square A$~$.

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

We conclude that $~$M\models\square[A\to B]\to(\square A \to \square B)$~$, no matter what $~$M$~$ is. %%

Those two last exercises prove that the [ K system] of modal logic is [soundness 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 [adequacy adequate]. You can check the proofs of adequacy in their respective pages.

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 %%note:Same for reflexive, symmetric and euclidean %%. Similarly, a Kripke model is finite if its set of worlds is finite.