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 $~$M$~$ is formed by three elements:

• A set of worlds $~$W$~$
• A visibility relationship between worlds $~$R$~$. If $~$wRx$~$, 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.

[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:

• If $~$A$~$ is a sentence letter $~$p$~$, then $~$M,w\models p$~$ if $~$V(w,p)=\top$~$.
• 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\models A$~$ Iff $~$M,w\not\models B$~$ or $~$M,w\models C$~$.
• If $~$A$~$ is of the form $~$\square B$~$, then $~$M,w\models \square B$~$ if $~$M,x\models 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\models A$~$) if $~$M,w\models 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\models 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 $~$\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.

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