# 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.

# Definition

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).

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.

Parents: