Sémantique de Kripke

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

La sémantique de Kripke, développée par Saul Aaron Kripke, est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales.

Elle est fondée sur un univers de mondes possibles, c'est-à-dire que le modèle qui réalise la logique n'est pas constitué d'un seul ensemble, mais il se subdivise en « mondes » entre lesquels existe une relation d'accessibilité. Sachant qu'une modalité modifie une proposition en lui donnant une portée plus ou moins grande, cette relation d'accessibilité permet d'envisager les mondes où cette proposition modifiée par la modalité est encore valide.

Dans la suite, il sera essentiellement question des modèles pour la logique propositionnelle où les mondes sont constitués de paires de booléens {vrai,faux} ; pour les modèles du calcul des prédicats intuitionniste ou modal on utilise des univers qui sont des ensembles non vides dans lesquels on va interpréter les prédicats et les fonctions.

Définitions[modifier | modifier le code]

Cadre de Kripke[modifier | modifier le code]

Exemple de cadre de Kripke

Un cadre de Kripke est un couple (W, R), où W est un ensemble de mondes {wi} appelé parfois univers et où R est une relation binaire sur ces mondes. R est appelée la « relation d'accessibilité » du cadre. Un cadre de Kripke définit donc quels mondes sont accessibles depuis chacun des mondes du cadre. Un cadre de Kripke est habituellement représenté sous la forme d'un graphe orienté dont les mondes sont les sommets et dont la relation d'accessibilité définit les arcs.

Par exemple, (\mathbb{N}, <) est le cadre qui caractérise la relation d'ordre « strictement inférieur » sur les entiers naturels. Chaque entier y représente un monde et un monde est en relation avec un autre si et seulement si le nombre correspondant au premier monde est strictement inférieur au nombre correspondant au second.

Modèle de Kripke[modifier | modifier le code]

Exemple de modèle de Kripke

Un modèle de Kripke est un triplet (W, R, h) où W est un ensemble de mondes dit univers, R une relation binaire dite d'accessibilité et h une fonction de valuation sur les atomes[1] d'un langage propositionnel L. Pour chaque proposition p, h(p) est l'ensemble des mondes de Wp est vraie.

h : Atom(L) \to \wp (W)

\wp (W) est l'ensemble des parties de W.

Un modèle de Kripke est donc un cadre de Kripke où pour chaque monde on connaît la valeur des propositions atomiques d'un langage L. Un cadre de Kripke peut donc être commun à plusieurs modèles de Kripke distincts (disposant chacun d'une fonction de valuation h spécifique).

Sémantique des logiques modales normales[modifier | modifier le code]

Définition de la sémantique[modifier | modifier le code]

Exemple de modèle de Kripke et de quelques formules modales vraies dans ses mondes

D'une manière informelle, \Box\phi est définie comme étant vraie dans un monde w si et seulement si \phi est vraie dans tous les mondes accessibles depuis w et \Diamond \phi est vraie dans un monde w si et seulement s'il existe un monde w' accessible depuis w tel que \phi soit vraie dans le monde w' .

Considèrons un modèle de Kripke \mathcal{M} = {W, R, h} et supposons que la logique modale normale dispose d'une modalité universelle \Box. L'opérateur \models (appliqué au modèle \mathcal{M} et à un monde w) est défini formellement par induction sur la structure des formules de la façon suivante. Ici \phi et \psi sont des formules quelconques bien formées de la logique modale et \mathcal{M}, w\models \phi se lit « \phi est vraie dans le monde  w du modèle \mathcal{M}».

  • \mathcal{M}, w \models p si et seulement si w \in h(p) (où p est un atome de L).
  • \mathcal{M}, w \models \top
  • \mathcal{M}, w \models \neg \phi si et seulement si \mathcal{M}, w \not\models \phi
  • \mathcal{M}, w \models \phi \vee \psi si et seulement si \mathcal{M}, w \models \phi ou \mathcal{M}, w \models \psi
  • \mathcal{M}, w \models \Box \phi si et seulement si  w R w' implique  \mathcal{M}, w' \models \phi

Si l'on donne aux abréviations ∧, → et \Diamond leurs définitions habituelles, les propriétés suivantes sont satisfaites :

  • \mathcal{M}, w \models \phi \wedge \psi si et seulement si \mathcal{M}, w \models \phi et \mathcal{M}, w \models \psi
  • \mathcal{M}, w \models \phi \to \psi si et seulement si (si \mathcal{M}, w \models \phi alors \mathcal{M}, w \models \psi)
  • \mathcal{M}, w \models \Diamond \phi si et seulement si \exists w', w R w' \wedge \mathcal{M}, w' \models \phi

L'expression \mathcal{M}, w \models \phi est parfois notée comme suit :

  • \mathcal{M} \models \phi(w)
  • \mathcal{M}, w \Vdash \phi
  • \mathcal{M} \models_w \phi
  • \|\phi\|^\mathcal{M}_w = 1

Validité, satisfaisabilité, équivalence[modifier | modifier le code]

  • Une formule \phi est Kripke-valide si et seulement si elle est vraie en tout monde de tout modèle de Kripke, on le note \models \phi:
\forall \mathcal{M}, \forall w, \mathcal{M}, w \models \phi
  • Une formule \phi est Kripke-satisfaisable si et seulement s'il existe un monde w d'un modèle M\phi est vraie :
\exists \mathcal{M}, \exists w, \mathcal{M}, w \models \phi
  • Une formule \phi est Kripke-équivalente à une formule \psi si et seulement si pour tout monde w de tout modèle M, \phi est vraie si et seulement si \psi est vraie :
\forall \mathcal{M}, \forall w, (\mathcal{M}, w \models \phi) implique et est impliquée par (\mathcal{M}, w \models \psi)

À titre d'exemple, la formule de Kripke (axiome K commun à toutes les logiques modales normales) est Kripke-valide :

\models\Box(\phi \to \psi) \to (\Box \phi \to \Box \psi)


On peut également définir les notions de validité, de satisfaisabilité et d'équivalence en se restreignant à un modèle, à un cadre ou à une classe de cadre, plutôt qu'à l'ensemble des modèles :

  • Une formule est valide dans un modèle si et seulement si elle est vraie en tout monde de ce modèle ;
  • Une formule est valide dans un cadre si et seulement si elle est valide dans tout modèle basé sur ce cadre ;
  • Une formule est valide dans une classe de cadres si et seulement si elle est valide dans tout cadre de la classe.

Ces dernières définitions permettent d'exprimer des vérités contingentes, par opposition à des vérités absolues (en logique modale normale) représentées par la Kripke-validité.

Correspondance et complétude[modifier | modifier le code]

Les propriétés de la relation d'accessibilité qui caractérise un cadre de Kripke sont étroitement liées aux axiomes de la modalité qui doit y trouver sa sémantique : n'importe quel cadre de Kripke ne peut pas représenter n'importe quelle logique modale. Henrik Sahlqvist a donné une correspondance précise entre certains types de formules (les formules de Sahlqvist) et l'expression en logique du premier ordre de propriétés sur la relation d'accessibilité : une formule de Sahlqvist est valide dans la classe des cadres de Kripke dont la relation d'accessibilité vérifie cette propriété.

Par exemple, la formule \Box \phi \to \phi ne peut être valide que lorsque le monde courant est accessible depuis lui-même : en fait cette formule est valide dans tous les cadres de Kripke dont la relation d'accessibilité est réflexive. L'algorithme de Sahlqvist, associé à cette correspondance, permet de déterminer l'expression caractérisant la relation d'accessibilité, à partir de la formule modale. Le tableau suivant donne les propriétés de relations associées à des formules courantes en logique modale normale :

Nom de la formule Formule de Sahlqvist Nom de la propriété Propriété de la relation
D \Box \phi \to \Diamond \phi Sérialité \forall w \in W, \exists w' \in W, w R w'
T ou M \Box \phi \to \phi Réflexivité \forall w \in W, w R w
4 \Box \phi \to \Box \Box \phi Transitivité \forall w, w', w'' \in W, w R w' \wedge w' R w'' \to w R w''
B \phi \to \Box \Diamond \phi Symétrie \forall w, w' \in W, w R w' \to w' R w
5 ou E \Diamond \phi \to \Box \Diamond \phi Caractère euclidien \forall w, w', w'' \in W, w R w' \wedge w R w'' \to w' R w''
CD \Diamond \phi \to \Box \phi Caractère fonctionnel, ou unicité, ou linéarité à droite \forall w, w', w'' \in W, w R w' \wedge w R w'' \to w' = w''
\Box M \Box(\Box \phi \to \phi) Pseudo-réflexivité \forall w, w' \in W, w R w' \to w' R w'
C4 \Box \Box \phi \to \Box \phi Densité \forall w, w' \in W, w R w' \to \exists w'' \in W, w R w'' \wedge w'' R w'
C ou G \Diamond \Box \phi \to \Box \Diamond \phi Confluence, convergence, ou incestualité \forall w, w', w'' \in W, w R w' \wedge w R w'' \to \exists w''' \in W, w' R w''' \wedge w'' R w'''

On peut noter que la formule de Kripke, ou formule de distribution (\Box (\phi \to \psi) \to (\Box \phi \to \Box \psi) n'est pas une formule de Sahlqvist, et ne correspond à aucune propriété de relation binaire : elle est valide dans tout cadre de Kripke, quelle que soit sa relation d'accessibilité.

Le théorème de Sahlqvist dit que tout système de logique modale normale K\Sigma, construit avec l'axiome de Kripke et un ensemble \Sigma d'axiomes choisis parmi les formules de Sahlqvist, est fortement complet pour la classe F_\Sigma des cadres de Kripke caractérisée par les propriétés du premier ordre associées aux formules de \Sigma. C'est-à-dire que pour tout ensemble de formules \Gamma \cup \{\phi\} appartenant au langage de K\Sigma, si \Gamma \models_{F_\Sigma} \phi, alors \Gamma \vdash_{K\Sigma} \phi. Dans ce formalisme, \Gamma \models_{F_\Sigma} \phi signifie qu'en tout monde w de tout modèle M de la classe de cadres F_\Sigma, si \mathcal{M}, w \models \Gamma alors \mathcal{M}, w \models \phi.

On dispose évidemment de la correction (si \Gamma \vdash_{K\Sigma} \phi, alors \Gamma \models_{F_\Sigma} \phi), par construction de la sémantique.


p-morphismes et bisimulations[modifier | modifier le code]

Pour plus de clarté, dans cette partie les mondes seront notés t, u ou v.

un p-morphisme est une application d'un ensemble de mondes dans un autre ensemble de mondes. Si l'on considère deux cadres de Kripke F = (W, R) et F' = (W' , R' ), et f une telle application, f est un p-morphisme de cadres de F dans F' si les deux conditions suivantes sont vérifiées :

  • t, u \in W \wedge t R u \to f(t) R' f(u)
  • (t \in W \wedge x \in W' \wedge f(t) R' x) \to \exists u \in W, t R u \wedge f(u) = x

De même, f est un p-morphisme de modèles d'un modèle M (basé sur le cadre F) dans un modèle M' (basé sur le cadre F' ) si :

  • f est un p-morphisme de cadres de F dans F'  ;
  • Pour un atome p et un monde t de W, \mathcal{M}, t \models p si et seulement si \mathcal{M'}, f(t) \models p

Les p-morphismes ont la propriété de préserver les formules modales et leur validité sur les cadres de Kripke, et peuvent être utilisés pour démontrer que certaines propriétés ne sont pas exprimables en logique modale.

Le terme bisimulation a un sens particulier en logique modale, dans le cadre de la sémantique de Kripke. Si l'on considère deux modèles de Kripke (W, R, h) et (W' , R' , h' ), une bisimulation entre M, u et M', u' est une relation binaire entre les mondes de W et les mondes de W' qui vérifie les propriétés suivantes si l'on considère que u B u' :

  • Pour tout atome p, \mathcal{M}, u \models p si et seulement si \mathcal{M'}, u' \models p
  • (v \in W \wedge u R v) \to \exists v' \in W', u' R v' \wedge v B v'
  • (v' \in W' \wedge u' R' v') \to \exists v \in W, u R v \wedge v' B v

Deux mondes (M, t) et (M' , t' ) sont dits bisimilaires s'il existe une bisimulation les mettant en relation l'un avec l'autre

Les bisimulations préservent également la validité des formules modales et permettent d'établir un lien entre logique modale et concurrence. La préservation des formules du premier ordre par les bisimulations permettent de caractériser l'ensemble des formules du premier ordre exprimables en logique modale, et donc de préciser le pouvoir d'expression de cette dernière.

Exemples[modifier | modifier le code]

Sémantique des logiques modales normales simples[modifier | modifier le code]

Dans les différentes logiques modales, la relation d'accessibilité de la sémantique de Kripke prend des sens différents.

  • En logique aristotélicienne (ou aléthique), les mondes accessibles depuis le monde w sont les mondes « possibles ». C'est l'origine de l'expression « sémantique des mondes possibles », qui est de fait abusive pour toutes les autres logiques modales.
  • En logique doxastique, les mondes accessibles depuis le monde w sont les mondes qui sont compatibles avec les croyances d'un agent se trouvant au monde w. Par exemple, si l'agent i croit uniquement que \phi est vraie (Bel_i \phi), alors les mondes accessibles seront ceux où \phi est effectivement vraie. Comme la relation n'est en général pas réflexive, le monde w n'est pas forcément accessible, donc \phi n'y est pas forcément vraie, ce qui modélise bien le fait que l'agent peut se tromper sur la réalité du monde dans lequel il est (ce monde actuel n'est pas forcément compatible avec ses croyances).
  • En logique épistémique, de manière assez similaire à la logique doxastique, les mondes accessibles depuis le monde courant sont ceux qui sont compatibles avec les connaissances de l'agent. Si l'agent sait uniquement que \phi est vraie, ce qui s'écrit (K_i \phi), alors les mondes accessibles seront ceux où \phi est vraie. En logique épistémique, la relation d'accessibilité est réflexive, et donc le monde courant est accessible, ce qui modélise le fait que lorsqu'un agent sait qu'une formule est vraie, il ne se trompe pas (sinon la connaissance redevient croyance).
  • En logique déontique, les mondes accessibles depuis un monde w sont ceux qui sont compatibles avec les normes, ou formules déontiques (obligations, permissions, interdictions...), qui sont vraies au monde w. Les mondes accessibles sont ceux qui respectent les normes, ce sont des mondes « idéaux ». Si au monde w les seules formules déontiques vraies disent que \phi est obligatoire et que \psi est interdite (Ob \phi, F \psi), alors les mondes accessibles seront tous ceux où \phi est vraie et \psi est fausse.

Dans chacune de ces logiques, le sens que l'on donne aux mondes peut varier, entraînant des variations plus ou moins fortes sur le sens de la relation d'accessibilité.

Sémantique des logiques temporelles linéaires (LTL)[modifier | modifier le code]

Exemple de modèle en logique temporelle linéaire

Les logiques temporelles linéaires sont une famille de logiques où les mondes (notés ici t, t' et à suivre, appartenant à l'ensemble T) représentent des instants, organisés en une chaîne unique orienté du passé vers le futur. La relation d'accessibilité de ces sémantiques est en général transitive, c'est-à-dire que les mondes accessibles depuis un monde t représentent tous les instants qui lui sont postérieurs.

Cette relation d'accessibilité R correspond à la modalité universelle G, G \phi signifiant que \phi sera vrai à tout instant du futur. Si G \phi est vraie à un monde t, on vérifie bien que \phi est vraie dans tous les mondes accessibles depuis t, c'est-à-dire à tous les instants postérieurs à t. La modalité existentielle associée est F, désignant le fait qu'il existe un instant futur où la formule considérée sera vraie. Formellement, la sémantique de ces opérateurs s'exprime comme suit :

\mathcal{M}, t \models G \phi si et seulement si \forall t' \in T, t R t' \to \mathcal{M}, t' \models \phi
\mathcal{M}, t \models F \phi si et seulement si \exists t' \in T, t R t' \wedge \mathcal{M}, t' \models \phi

À l'image de G et F, on peut introduire les modalités H et P pour le passé : H \phi dit que \phi a été vrai à tout instant du passé, et P \phi qu'il existe un instant du passé où \phi a été vraie. On peut définir la sémantique de H et P en se basant uniquement sur la relation R :

\mathcal{M}, t \models H \phi si et seulement si \forall t' \in T, t' R t \to \mathcal{M}, t' \models \phi
\mathcal{M}, t \models P \phi si et seulement si \exists t' \in T, t' R t \wedge \mathcal{M}, t' \models \phi

On introduit souvent les modalités binaires \mathcal{U} (until, jusqu'à) et \mathcal{S} (since, depuis), qui apportent énormément d'expressivité au langage[2]. \phi \mathcal{U} \psi signifie que \phi est vraie jusqu'à ce que \psi soit vraie, et \phi \mathcal{S} \psi signifie que \phi a été vraie depuis que \psi ne l'est plus. La caractérisation de leur sémantique est la suivante :

\mathcal{M}, t \models \phi \mathcal{U} \psi si et seulement si \exists t' \in T, t R t' \wedge \mathcal{M}, t' \models \psi et \forall t'', (t R t'' \wedge t'' R t') \to \mathcal{M}, t'' \models \phi
\mathcal{M}, t \models \phi \mathcal{S} \psi si et seulement si \exists t' \in T, t' R t \wedge \mathcal{M}, t' \models \psi et \forall t'', (t' R t'' \wedge t'' R t) \to \mathcal{M}, t'' \models \phi

On peut également définir d'autres modalités pour les logiques temporelles linéaires, en introduisant des relations d'accessibilité complémentaires. Ainsi, X \phi désigne le fait que \phi est vraie à l'instant suivant. X est une modalité universelle, associée à une relation d'accessibilité R_X qui met en relation un instant et le suivant (et aucun autre).

Sémantique de la logique CTL[modifier | modifier le code]

Exemple de modèle en logique CTL

Dans les logiques temporelles arborescentes, comme la logique CTL (pour Computational Tree Logic), chaque instant a plusieurs successeurs possibles, ce qui permet d'exprimer la notion de point de choix. Pour chaque branche de l'arbre, on retrouve les notions de la logique temporelle linéaire. Pour travailler sur l'arborescent, on utilise les préfixes modaux A (modalité universelle désignant tous les chemins possibles à partir de l'instant courant) et E (modalité existentielle désignant un chemin possible et existant à partir de l'instant courant). Ces préfixes sont toujours suivis des modalités X, F, G ou U de la logique temporelle linéaire.

La sémantique de la logique CTL utilise une relation d'accessibilité R de proche en proche, qui à chaque instant relie les instants suivants possibles. C'est la relation d'accessibilité de la modalité universelle AX et de sa modalité existentielle associée EX :

\mathcal{M}, t \models AX \phi si et seulement si \forall t' \in T, t R t' \to \mathcal{M}, t' \models \phi
\mathcal{M}, t \models EX \phi si et seulement si \exists t' \in T, t R t' \wedge \mathcal{M}, t' \models \phi

À partir de la relation R, on définit la notation suivante pour les chemins possibles :

<t_1, t_2, ... t_n> \leftrightarrow t_1 R t_2 \wedge ... \wedge t_n R t'

À l'aide des chemins, on construit ainsi la sémantique des autres modalités de CTL :

\mathcal{M}, t \models AG \phi si et seulement si \forall t_1, t_2, ... \in T, <t, t_1, ...> \to \forall i \in \mathbb{N}^*, \mathcal{M}, t_i \models \phi
\mathcal{M}, t \models EG \phi si et seulement si \exists t_1, t_2, ... \in T, <t, t_1, ...> \wedge \forall i \in \mathbb{N}^*, \mathcal{M}, t_i \models \phi
\mathcal{M}, t \models AF \phi si et seulement si \forall t_1, t_2, ... \in T, <t, t_1, ...> \to \exists i \in \mathbb{N}^*, \mathcal{M}, t_i \models \phi
\mathcal{M}, t \models EF \phi si et seulement si \exists t_1, t_2, ... \in T, <t, t_1, ...> \wedge \exists i \in \mathbb{N}^*, \mathcal{M}, t_i \models \phi
\mathcal{M}, t \models A (\phi \mathcal{U} \psi) si et seulement si \forall t_1, t_2, ... \in T, <t, t_1, ...> \to \exists i \in \mathbb{N}^*, ((\mathcal{M}, t_i \models \psi) \wedge (\forall j \in \mathbb{N}^*, i<j \to \mathcal{M}, t_j \models \phi))
\mathcal{M}, t \models E (\phi \mathcal{U} \psi) si et seulement si \exists t_1, t_2, ... \in T, <t, t_1, ...> \wedge \exists i \in \mathbb{N}^*, ((\mathcal{M}, t_i \models \psi) \wedge (\forall j \in \mathbb{N}^*, i<j \to \mathcal{M}, t_j \models \phi))

Sémantique de la logique PDL[modifier | modifier le code]

En logique dynamique et dans la logique PDL en particulier, on considère que les mondes représentent les états possibles d'une machine qui exécute des programmes \pi \in P.

  • [\pi]\phi signifie que \phi est vraie après toute exécution possible de \pi ;
  • <\pi>\phi signifie qu'il existe une exécution de \pi après laquelle \phi est vraie ;
  • \pi_1 ; \pi_2 désigne la succession des deux programmes \pi_1 et \pi_2 ;
  • \phi ? est un programme qui s'exécute avec succès sans changement d'état si et seulement si \phi est vraie.

Chaque programme \pi ayant sa propre modalité universelle, il y a donc autant de relations d'accessibilité R_\pi que de programmes dans P. Les cadres de Kripke correspondants sont donc un peu particulier, puisqu'ils disposent d'une classe de relations, au lieu d'une relation unique.

La sémantique de la relation d'accessibilité est la suivante : pour deux mondes w et w', w R_\pi w' si et seulement si lorsque la machine est dans l'état w, elle peut exécuter \pi et se retrouver dans l'état w'.

Les relations entre les différentes relations d'accessibilité se formalisent ainsi :

  • w R_{\pi_1 \cup \pi_2} w' si et seulement si w R_{\pi_1} w' ou w R_{\pi_2} w' ;
  • w R_{\pi_1 \cap \pi_2} w' si et seulement si w R_{\pi_1} w' et w R_{\pi_2} w' ;
  • w R_{\pi_1 ; \pi_2} w' si et seulement si \exists w'' \in W, w R_{\pi_1} w'' \wedge w'' R_{\pi_2} w' ;
  • R_{\pi^*} est la fermeture réflexive transitive de R_\pi ;
  • w R_{\phi?} w' si et seulement si w = w' et \mathcal{M}, w \models \phi.

Sémantique de la logique intuitionniste[modifier | modifier le code]

La logique intuitionniste peut-être vue comme une logique modale, elle a donc une sémantique de Kripke qui est expliquée dans l'article consacré à la logique intuitionniste.

Notes et références[modifier | modifier le code]

  1. Une formule atomique ou atome, est une formule qui ne contient pas de sous-formules.
  2. Sur la classe des flots de temps complets au sens de Dedekind, l'expressivité de la logique US est identique à celle de la logique du premier ordre. D'autre part, toutes les autres modalités de la logique temporelle peuvent s'exprimer à l'aide de \mathcal{U} et \mathcal{S}

Voir aussi[modifier | modifier le code]