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

bewerken

Formeel is een Kripkemodel   een geordend drietal   waarbij   een verzameling "werelden" (of punten) is,   een relatie op   (de toegankelijkheidsrelatie) en   een functie die aan een atomaire propositie   een verzameling werelden toekent waarin   waar is.

  wordt uitgebreid naar een waarheidsrelatie   tussen modellen, werelden en zinnen van de modale logica, als volgt:

  •   desda   (  een atomaire propositie)
  •   desda   (negatie)
  •   desda   en   (conjunctie)
  • (Soortgelijke regels voor disjunctie enz.)
  •   desda  

De laatste regel formaliseert het idee van noodzakelijke waarheid:   is waar in   dan en slechts dan als   waar is in alle met   verbonden werelden. Afhankelijk van hoe de relatie   geïnterpreteerd wordt, zijn dat bijvoorbeeld alle werelden die denkbaar zijn voor personen die in de wereld   leven, alle toekomstige werelden na  , alle wenselijke werelden, enz.

In de epistemische logica worden vaak uitgebreide Kripkemodellen gebruikt, die een hele verzameling toegankelijkheidsrelaties gebruiken (één per actor).

Voorbeeld

bewerken
 
Een Kripkemodel met een toegankelijksrelatie tussen de werelden w1, ..., w5.

Het weergegeven Kripkemodel kan worden gedefinieerd als:

 
 
 ,   voor  

In het gegeven voorbeeld gelden bijvoorbeeld de volgende formules in wereld  :

 ,
 ,
 .

Frame-eigenschappen

bewerken

De component   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   in elke wereld.

Bisimulatie

bewerken
  Zie Bisimulatie voor het hoofdartikel over dit onderwerp.

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 (  en  ,  ) maar ook voor modale formules, zoals   of  .

Zie de categorie Kripke models van Wikimedia Commons voor mediabestanden over dit onderwerp.