# Kripkemodel

Een Kripkemodel is een model voor modale logica's en andere niet-klassieke logica's zoals de intuïtionistische logica. Kripkemodellen danken hun naam aan hun uitvinder, Saul Kripke. Ze formaliseren het idee van meerdere mogelijke werelden.

## Definitie

Formeel is een Kripkemodel ${\mathcal {M}}$ een geordend drietal $\langle W,R,V\rangle$ waarbij $W$ een verzameling "werelden" (of punten) is, $R$ een relatie op $W$ (de toegankelijkheidsrelatie) en $V$ een functie die aan een atomaire propositie $p$ een verzameling werelden toekent waarin $p$ waar is.
$V$ wordt uitgebreid naar een waarheidsrelatie $\Vdash$ tussen modellen, werelden en zinnen van de modale logica, als volgt:
* ${\mathcal {M}},w\Vdash p$ desda $w\in V(p)$ ($p$ een atomaire propositie)
* ${\mathcal {M}},w\Vdash \neg A$ desda ${\mathcal {M}},w\not \Vdash A$ (negatie)
* ${\mathcal {M}},w\Vdash A\land B$ desda ${\mathcal {M}},w\Vdash A$ en ${\mathcal {M}},w\Vdash B$ (conjunctie)
* (Soortgelijke regels voor disjunctie enz.)
* ${\mathcal {M}},w\Vdash \Box A$ desda $\forall w'\in W(wRw'\to {\mathcal {M}},w'\Vdash A)$
De laatste regel formaliseert het idee van noodzakelijke waarheid: $A$ is waar in $w$ dan en slechts dan als $A$ waar is in alle met $w$ verbonden werelden. Afhankelijk van hoe de relatie $R$ geïnterpreteerd wordt, zijn dat bijvoorbeeld alle werelden die denkbaar zijn voor personen die in de wereld $w$ leven, alle toekomstige werelden na $w$, alle wenselijke werelden, enz.
In de epistemische logica worden vaak uitgebreide Kripkemodellen gebruikt, die een hele verzameling toegankelijkheidsrelaties gebruiken (één per actor).

## Voorbeeld

Het weergegeven Kripkemodel kan worden gedefinieerd als:
    $W=\{w_{1},w_{2},w_{3},w_{4},w_{5}\}$
    $R=\{(w_{1},w_{2}),(w_{2},w_{3}),(w_{2},w_{4}),(w_{3},w_{3}),(w_{3},w_{5}),(w_{4},w_{5})\}$
    $V(\phi )=\{w_{3},w_{4}\}$, $V(\psi )=\{\}$ voor $\psi \neq \phi$
In het gegeven voorbeeld gelden bijvoorbeeld de volgende formules in wereld $w_{1}$:
    ${\mathcal {M}},w_{1}\Vdash \neg \phi$,
    ${\mathcal {M}},w_{1}\Vdash \Box \neg \phi$,
    ${\mathcal {M}},w_{1}\Vdash \Diamond \Diamond \phi$.

## Frame-eigenschappen

De component $\langle W,R\rangle$ wordt het frame van een Kripkemodel genoemd. Dit frame kan bepaalde kenmerken hebben, zoals dat elke wereld w een toegankelijke wereld v heeft die te bereiken is vanuit w. Wanneer de relatie R bepaalde eigenschappen heeft dan zegt men dat het frame die ook heeft. Bijvoorbeeld: een frame is reflexief als de relatie R een reflexieve relatie is. In een reflexief frame gelden modale formules die niet hoeven te gelden op een frame die deze eigenschap niet heeft. In een reflexief frame geldt bijvoorbeeld $\Box p\rightarrow p$ in elke wereld.

## Bisimulatie

Het concept van bisimulatie wordt gebruikt om Kripkemodellen met elkaar te vergelijken: het idee dat is dat werelden in verschillende modellen bisimilair zijn als deze dezelfde propositionele en modale formules waarmaken. Anders gezegd gelden in dergelijke werelden dezelfde formules en is het mogelijk vanuit beide bisimilaire werelden naar dezelfde soort werelden te gaan via de toegankelijkheidsrelatie. Er zijn in dat geval geen modale formules die gebruikt kunnen worden om de werelden te onderscheiden: er is geen formule die wel geldt in de ene wereld maar niet in de andere. Als dit wel mogelijk is dan zijn de werelden niet bisimilair.
Een voorbeeld: stel we hebben een model M met een wereld w met een pijl naar zichzelf. In deze wereld geldt de atomaire formule p. We hebben ook een model N met een wereld v en een wereld u waarvoor geldt dat v toegankelijk is vanuit u en u is toegankelijk vanuit v. In zowel u als v geldt de formule p. Er geldt nu dat w bisimilair is met de wereld v en ook met de wereld u. Elke formule die geldt in w geldt ook in de wereld v en in de wereld u. Dit geldt voor de atomaire formules (${\mathcal {M}},w\Vdash p$ en ${\mathcal {N}},v\Vdash p$, ${\mathcal {N}},u\Vdash p$) maar ook voor modale formules, zoals ${\mathcal {M}},w\Vdash \Diamond p$ of ${\mathcal {M}},w\Vdash \Diamond \Diamond p$.