Kripke model

Kripke mod­els are in­ter­pre­ta­tions of modal logic which turn out to be ad­e­quate un­der some ba­sic con­straints for a wide ar­ray of sys­tems of modal logic.


A Kripke model \(M\) is formed by three el­e­ments:

  • A set of wor­lds \(W\)

  • A visi­bil­ity re­la­tion­ship be­tween wor­lds \(R\). If \(wRx\), we will say that \(w\) sees \(x\) or that \(x\) is a suc­ces­sor of \(w\).

  • A val­u­a­tion func­tion \(V\) that as­so­ci­ates pairs of wor­lds and sen­tence let­ters to truth val­ues.

You can vi­su­al­ize Kripke wor­lds as a di­graph in which each node is a world, and the edges rep­re­sent visi­bil­ity.

images of Kripke worlds

The val­u­a­tion func­tion can be ex­tended to as­sign truth val­ues to whole modal sen­tences. We will say that a world \(w\in W\) makes a modal sen­tence \(A\) true (no­ta­tion: \(M,w\models A\)) if it is as­signed a truth value of true ac­cord­ing to the fol­low­ing rules:

  • If \(A\) is a sen­tence let­ter \(p\), then \(M,w\models p\) if \(V(w,p)=\top\).

  • If \(A\) is a truth func­tional com­pound of sen­tences, then its value comes from the propo­si­tional calcu­lus and the val­ues of its com­po­nents. For ex­am­ple, 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 ev­ery suc­ces­sor \(x\) of \(w\).

Given this way of as­sign­ing truth val­ues to sen­tences, we will say the fol­low­ing:

  • \(A\) is valid in a model \(M\) (no­ta­tion: \(M\models A\)) if \(M,w\models A\) for ev­ery \(w\) in \(W\).

  • \(A\) is valid in a class of mod­els if it is valid in ev­ery model of the class.

  • \(A\) is satis­fi­able in a model \(M\) if there ex­ists \(w\in W\) such that \(M,w\models A\).

  • \(A\) is satis­fi­able in a class of mod­els if it is satis­fi­able in some model of the class.

No­tice that a sen­tence \(A\) is valid in a class of mod­els iff its nega­tion is not satis­fi­able.

Kripke mod­els as se­man­tics of modal logic

Kripke mod­els are tightly con­nected to the in­ter­pre­ta­tions of cer­tain modal log­ics.

For ex­am­ple, they model well the rules of nor­mal prov­abil­ity sys­tems.

Ex­er­cise: show that Kripke mod­els satisfy the ne­ces­si­ta­tion rule of modal logic. That is, if \(A\) is valid in \(M\), then \(\square A\) is valid in \(M\).

Let \(w\inW\) be a world of \(M\). Let \(x\) be an ar­bi­trary suc­ces­sor of \(w\). Then, as \(M\models A\), then \(M,x\models A\). Since \(x\) was ar­bi­trary, ev­ery suc­ces­sor of \(w\) mod­els \(A\), so \(w\models \square A\). As \(w\) was ar­bi­trary, then ev­ery world in \(M\) mod­els \(\square A\), and thus \(M\models \square A\).

Ex­er­cise: Show that the dis­tribu­tive ax­ioms are always valid in Kripke mod­els. Distribu­tive ax­ioms are modal sen­tences of the form \(\square[A\to B]\to(\square A \to \square B)\).

Sup­pose that \(w\in W\) is such that \(w\models \square[A\to B]\) and \(w\models \square A\).

Let \(x\) be a suc­ces­sor of \(w\). Then \(x\models A\to B\) and \(x\models A\). We con­clude by the propo­si­tional calcu­lus that \(x\models B\), so as \(x\) was an ar­bi­trary suc­ces­sor we have that \(w\models \square B\), and thus \(w\models\square[A\to B]\to(\square A \to \square B)\).

We con­clude that \(M\models\square[A\to B]\to(\square A \to \square B)\), no mat­ter what \(M\) is. <div><div>

Those two last ex­er­cises prove that the K sys­tem of modal logic is sound for the class of all Kripke mod­els. This is be­cause we have proved that its ax­ioms and rules of in­fer­ence hold in all Kripke mod­els (propo­si­tional tau­tolo­gies and modus po­nens triv­ially hold).

Some ad­e­quacy theorems

Now we pre­sent a re­la­tion of modal log­ics and the class of Kripke mod­els in which they are ad­e­quate. You can check the proofs of ad­e­quacy in their re­spec­tive pages.

  • The class of all Kripke mod­els is ad­e­quate to the K system

  • The class of tran­si­tive Kripke mod­els is ad­e­quate to K4

  • The class of re­flex­ive Kripke mod­els is ad­e­quate to T

  • The class of re­flex­ive and tran­si­tive Kripke mod­els is ad­e­quate to S4

  • The class of re­flex­ive and sym­met­ric Kripke mod­els is ad­e­quate to B

  • The class of re­flex­ive and eu­clidean Kripke mod­els is ad­e­quate to S5

  • The class of finite, ir­reflex­ive and tran­si­tive Kripke mod­els is ad­e­quate to GL

No­tice that as the con­straint on the mod­els be­comes stronger, the set of valid sen­tences in­creases, and thus the cor­re­spon­dent ad­e­quate sys­tem is stronger.

A note about no­ta­tion may be in or­der. We say that a Kripke model is, e.g, tran­si­tive if its visi­bil­ity re­la­tion is tran­si­tive noteSame for re­flex­ive, sym­met­ric and eu­clidean . Similarly, a Kripke model is finite if its set of wor­lds is finite.