En logique mathématique, la sémantique de Kripke est une sémantique formelle utilisée pour les logiques non-classiques comme la logique intuitionniste et certaines logiques modales. Elle a été développée à la fin des années 1950 et début des années 1960 par Saul Kripke et est fondée sur la théorie des mondes possibles.
Définitions
Cadre de Kripke
Un cadre de Kripke est un couple (W, R), où W est un ensemble de mondes appelés parfois mondes possibles et où R est une relation binaire sur W. L'ensemble W s'appelle parfois l'univers des mondes possibles. La relation R est appelée relation d'accessibilité 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é donne les arcs. Une telle relation R définit les mondes accessibles depuis chaque monde. Dans l'exemple ci-contre, et sont les deux mondes accessibles depuis .
La structure (, <), c'est-à-dire l'ensemble des entiers naturels muni est de la relation d'ordre « strictement inférieur », est un autre exemple de cadre. Chaque entier est un monde possible 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
Un modèle de Kripke est un triplet (W, R, h) où (W, R) est un cadre de Kripke, et h une fonction, qui indique pour chaque variable propositionnelle p, l'ensemble des mondes de W où p est vraie. 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
Définition de la sémantique
De manière informelle, la formule de la logique modale est définie comme étant vraie dans un monde w si et seulement si est vraie dans tous les mondes accessibles depuis w. La formule est vraie dans un monde w si et seulement s'il existe un monde w' accessible depuis w tel que soit vraie dans le monde w' .
Considérons un modèle de Kripke = {W, R, h} et supposons que la logique modale normale dispose d'une modalité universelle . L'opérateur (appliqué au modèle et à un monde w) est défini formellement par induction sur la structure des formules de la façon suivante. Ici et sont des formules quelconques bien formées de la logique modale et se lit « est vraie dans le monde du modèle » ou « réalise la formule dans le modèle »
si et seulement si (où est une variable propositionnelle).
si et seulement si si et seulement si ou si et seulement si implique
Si l'on donne aux abréviations ∧, → et leurs définitions habituelles, les propriétés suivantes sont satisfaites : si et seulement si et si et seulement si (si alors ) si et seulement si
L'expression est parfois notée comme suit :
Validité, satisfaisabilité, équivalence
Une formule est Kripke-valide si et seulement si elle est vraie en tout monde de tout modèle de Kripke, on le note :
Une formule est Kripke-satisfaisable si et seulement s'il existe un monde w d'un modèle M où est vraie :
Une formule est Kripke-équivalente à une formule si et seulement si pour tout monde w de tout modèle M, est vraie si et seulement si est vraie : implique et est impliquée par
À titre d'exemple, la formule de Kripke (axiome K commun à toutes les logiques modales normales) est Kripke-valide :
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
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 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 relationDSérialitéT ou M ou Réflexivité4 ou TransitivitéBSymétrie5 ou ECaractère euclidienCDCaractère fonctionnel, ou unicité, ou linéarité à droitePseudo-réflexivitéC4 ou DensitéC ou GConfluence, ou propriété de Church-Rosser
On peut noter que la formule de Kripke, ou formule de distribution ( 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 , construit avec l'axiome de Kripke et un ensemble d'axiomes choisis parmi les formules de Sahlqvist, est fortement complet pour la classe des cadres de Kripke caractérisée par les propriétés du premier ordre associées aux formules de . C'est-à-dire que pour tout ensemble de formules appartenant au langage de , si , alors . Dans ce formalisme, signifie qu'en tout monde w de tout modèle M de la classe de cadres , si alors .
On dispose évidemment de la correction (si , alors ), par construction de la sémantique.
p-morphismes et bisimulations
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 :
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, si et seulement si
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 : Pour tout atome p, si et seulement si
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
Sémantique des logiques modales normales simples
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 est vraie (), alors les mondes accessibles seront ceux où 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 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 est vraie, ce qui s'écrit (), alors les mondes accessibles seront ceux où 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 est obligatoire et que est interdite (), alors les mondes accessibles seront tous ceux où est vraie et 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)
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, signifiant que sera vrai à tout instant du futur. Si est vraie à un monde t, on vérifie bien que 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 : si et seulement si si et seulement si
À l'image de G et F, on peut introduire les modalités H et P pour le passé : dit que a été vrai à tout instant du passé, et qu'il existe un instant du passé où a été vraie. On peut définir la sémantique de H et P en se basant uniquement sur la relation R : si et seulement si si et seulement si