Logique épistémique

La logique épistémique est une logique modale qui permet de raisonner à propos de la connaissance d'un ou plusieurs agents. Elle permet aussi de raisonner sur les connaissances des connaissances des autres agents, etc. Son nom est tiré du nom grec epistḗmē qui signifie « connaissance » (du verbe epístamai « savoir »), d'où vient aussi le mot épistémologie. L'application de la logique épistémique à l'économie a été promue par Robert Aumann, Prix Nobel d'économie 2005.

Historique[modifier | modifier le code]

Elle a été introduite par Edward John Lemmon (en) et Jaakko Hintikka. Elle est complétée par la logique de la connaissance commune qui met en œuvre plusieurs agents.

Définition[modifier | modifier le code]

Nous ne présentons que la logique épistémique propositionnelle.

Syntaxe[modifier | modifier le code]

On introduit une modalité $K_{i}$ pour chaque agent $i$ . La construction $K_{i}(\phi )$ signifie intuitivement que l'agent $i$ sait $\phi$ .

Sémantique[modifier | modifier le code]

Les modèles de la logique épistémique sont les modèles de Kripke.

Présentation intuitive[modifier | modifier le code]

L'idée de Kripke est d'introduire des mondes possibles. Dans chaque monde, une relation (dite réalisabilité) indique quelles propositions atomiques sont vraies et quelles propositions atomiques sont fausses. En particulier, le monde actuel (réel) est un monde possible. Dans un monde possible donné, un agent imagine d'autres mondes comme possibles ou envisageables. Pour cela, une relation d'indistinguabilité est introduite pour chaque agent. S'il y a n agents, il y a donc n relations d'accessibilité étiquetée chacune par le nom de l'agent.

Présentation formelle[modifier | modifier le code]

Dans un modèle de Kripke, on distingue:

un univers ${\mathcal {U}}$ dont les éléments notés $m$ sont appelés des mondes,

pour chaque agent $i$ une relation $\equiv _{i}$ dite relation d'accessibilité pour $i$ ,

une relation $\Vdash$ de réalisabilité entre un monde $m$ et une proposition $\varphi$ , on écrit $m\Vdash \varphi$ et on lit $m$ réalise $\varphi$ .

Un cône est un ensemble $C$ de mondes ( $C\subseteq {\mathcal {U}}$ ) tels

si $m\in C$
et si pour tout $i$ entre $1$ et $n$ , on a $m\equiv _{i}m'$ ,

alors $m'\in C$ .

Une initialisation est une application $I$ qui associe à chaque variable un cône de ${\mathcal {U}}$ .

Le triplet ${\mathcal {M}}=\langle {\mathcal {U}}_{\mathcal {M}},\{\equiv _{1},...,\equiv _{n}\},I_{\mathcal {M}}\rangle$ s'appelle un modèle ou une structure de Kripke. S'il n'y a pas d'ambiguïté on abandonne les indices ${\mathcal {M}}$ .

La relation de réalisabilité, notée $\Vdash _{\mathcal {M}}$ , ou $\Vdash$ quand il n'y a pas d'ambiguïté, se définit par induction sur la structure des propositions.

Si $\varphi$ est une variable $x$ , $m\Vdash x$ si et seulement si $m\in I$ .
Si $\varphi =K_{i}(\psi )$ , alors $m\Vdash \varphi$ si et seulement pour tout monde $m'\in {\mathcal {U}}$ tel que $m\equiv _{i}m'$ on a $m'\Vdash \psi$ .
Si $\varphi =\varphi _{1}\vee \varphi _{2}$ , $m\Vdash \varphi$ si et seulement si $m\Vdash \varphi _{1}$ ou $m\Vdash \varphi _{2}$ .
Et ainsi de suite pour chaque connecteur.

On dit que $\varphi$ est valide dans ${\mathcal {M}}$ ou que ${\mathcal {M}}$ modélise $\varphi$ , noté ${\mathcal {M}}\vDash \varphi$ , si pour $m\in {\mathcal {U}}_{\mathcal {M}}$ , on a $m\Vdash \varphi$ .

Validité[modifier | modifier le code]

Une proposition $\varphi$ est valide (noté $\vDash \varphi$ ) si pour tout modèle ${\mathcal {M}}$ on a ${\mathcal {M}}\vDash \varphi$ . Autrement dit, une proposition $\varphi$ est valide si pour tout modèle ${\mathcal {M}}$ et tout monde $m$ dans ce modèle, $m\Vdash \varphi$ .

Les règles et les axiomes[modifier | modifier le code]

La logique épistémique se formalise plus facilement en utilisant une approche à la Hilbert (les seules formules auxquelles on s'intéresse sont les théorèmes). Dans ce qui suit $\vdash \varphi$ doit se lire « $\varphi$ est un théorème». La logique épistémique satisfait les axiomes de la logique modale, mais avec une signification différente (voir ci-dessus). Certains philosophes n'acceptent que certains parmi les axiomes qui suivent, notamment parmi T, 4 et 5.

Les règles[modifier | modifier le code]

${\frac {\vdash _{taut}\varphi }{\vdash \varphi }}$ Tautologie où $\vdash _{taut}\varphi$ signifie que $\varphi$ est une tautologie classique (ou intuitionniste).

${\frac {\vdash \varphi \Rightarrow \psi \qquad \vdash \varphi }{\vdash \psi }}$ modus ponens

${\frac {\vdash \varphi }{\vdash K_{i}(\varphi )}}$ règle de nécessitation ou de généralisation

Les axiomes[modifier | modifier le code]

$\vdash K_{i}(\varphi \Rightarrow \psi )\Rightarrow (K_{i}(\varphi )\Rightarrow K_{i}(\psi ))$ axiome de distribution ou axiome K.

$\vdash K_{i}(\varphi )\Rightarrow \varphi$ axiome de la connaissance ou axiome T ou encore axiome de vérité.

$\vdash K_{i}(\varphi )\Rightarrow K_{i}(K_{i}(\varphi ))$ axiome d'introspection positive ou 4.

$\vdash \neg K_{i}(\varphi )\Rightarrow K_{i}(\neg K_{i}(\varphi ))$ axiome d'introspection négative ou 5.

La signification des règles et des axiomes[modifier | modifier le code]

La règle Tautologie dit que toutes les propositions qui sont des théorèmes (c'est-à-dire des tautologies) de la logique classique (ou intuitionniste) sont des théorèmes de la logique épistémique.

Le modus ponens est la règle bien connue depuis Aristote qui permet de faire des déductions.

La règle de généralisation signifie que les agents raisonnent parfaitement et sont à même de connaître tous les faits pour lesquels il existe une démonstration.

L'axiome K montre comment l'agent peut faire des déductions à partir de ce qu'il connaît.

L'axiome T dit que les agents ne connaissent que des choses « vraies », autrement dit, si un agent connaît quelque chose alors cette chose est vraie.

L'axiome 4 dit que si un agent sait quelque chose, alors il sait qu'il le sait.

L'axiome 5 dit que si un agent ne sait pas quelque chose, alors il sait qu'il ne le sait pas.

T, S4 et S5[modifier | modifier le code]

Il y a différentes logiques épistémiques suivant les règles qui sont acceptées parmi celles qui viennent d'être présentées.

La logique $\mathbb {T}$ est formée des règles et des axiomes K et T. La logique $\mathbb {S} \mathbf {4}$ est $\mathbb {T}$ augmentée de 4. La logique $\mathbb {S} \mathbf {5}$ est $\mathbb {S} \mathbf {4}$ augmentée de 5.

Dans les logiques épistémiques on peut démontrer des grands méta-théorèmes de la logique mathématique.

Théorème de correction[modifier | modifier le code]

Toute proposition prouvable est valide. Autrement dit, si $\vdash \varphi$ alors $\vDash \varphi$ .

Complétude[modifier | modifier le code]

Complétude de T[modifier | modifier le code]

Si l'on considère les modèles où les relations d'accessibilité sont réflexives alors toute proposition valide est prouvable dans $\mathbb {T}$ .

Complétude de S4[modifier | modifier le code]

Si l'on considère les modèles où les relations d'accessibilité sont des relations de préordre (réflexives et transitives) alors toute proposition valide est prouvable dans $\mathbb {S} _{4}$ .

Complétude de S5[modifier | modifier le code]

Si l'on considère les modèles où les relations d'accessibilité sont des relations d'équivalence (réflexives, transitives et symétriques) alors toute proposition valide est prouvable dans $\mathbb {S} _{5}$ .

Sources[modifier | modifier le code]

J.-J. Ch. Meyer et W. van der Hoek, Epistemic Logic for Computer Science and Artificial Intelligence, volume 41, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1995 (ISBN 052146014X)

R. Fagin, J. Y. Halpern, Y. Moses et M. Y. Vardi, Reasoning About Knowledge, The MIT Press, 1995 (ISBN 0-262-56200-6)

Articles connexes[modifier | modifier le code]

Théorie de Dempster-Shafer