Logique épistémique
426283
31081167
2008-06-27T22:04:22Z
Thijs!bot
105469
robot Ajoute: [[ja:認識論理]]
La '''logique épistémique''' est la logique de la [[connaissance]] d'agents pris individuellement. Son nom vient du verbe grec ''epistémei'' qui signifie ''savoir'', qui a aussi produit le mot [[épistémologie]]. Ses créateurs sont [[E. J. Lemmon]] and [[Jaakko Hintikka]]. Elle est complétée par la [[logique de la connaissance commune]] qui met en œuvre plusieurs agents.
L'application de la logique épistémique à l'[[sciences économiques|économie]] a été promue par [[Robert Aumann]], [[Prix de la Banque de Suède en sciences économiques en mémoire d'Alfred Nobel|« Prix Nobel » d'économie]] 2005.
En logique épistémique il y a plusieurs agents qui ont la capacité de raisonner en prenant en compte la connaissance qu'ils ont de certaines propositions ou la connaissance des autres agents. C'est typiquement la logique d'un joueur qui raisonne sur son jeu.
La logique épistémique règle donc les aspects logiques ayant trait à la connaissance d'un agent. Ici nous ne présentons que la logique épistémique [[calcul des propositions|propositionnelle]]. Il existe une [[logique modale|modalité]] <math>K_i</math> pour chaque agent <math>i</math>. Ainsi <math>K_i(\phi)</math> signifie que ''l'agent <math>i</math> sait <math>\phi</math>''. La logique épistémique est donc une [[logique modale]]
==Les règles et les axiomes==
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 <math>\vdash \varphi</math> doit se lire «<math>\varphi</math> ''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===
*<math>\frac{\vdash_{taut}\varphi}{\vdash \varphi}</math> ''Tautologie'' où <math>\vdash_{taut}\varphi</math> signifie que <math>\varphi</math> est une tautologie [[:en:Wikipedia:classical logic|classique]] (ou [[Démonstration constructive|intuitionniste]]).
*<math>\frac{\vdash \varphi \Rightarrow \psi \qquad \vdash \varphi}{\vdash \psi}</math> ''modus ponens''
*<math>\frac{\vdash\varphi}{\vdash K_i(\varphi)}</math> règle de ''nécessitation'' ou de ''généralisation''
===Les axiomes===
*<math>\vdash K_i(\varphi \Rightarrow \psi) \Rightarrow (K_i(\varphi) \Rightarrow K_i(\psi))</math> ''axiome de distribution'' ou ''axiome'' '''K'''.
*<math>\vdash K_i(\varphi) \Rightarrow \varphi</math> ''axiome de la connaissance'' ou ''axiome'' '''T''' ou encore ''axiome de vérité''.
*<math>\vdash K_i(\varphi) \Rightarrow K_i(K_i(\varphi))</math> ''axiome d'introspection positive'' ou '''4'''.
*<math>\vdash \neg K_i(\varphi) \Rightarrow K_i( \neg K_i(\varphi))</math> ''axiome d'introspection négative'' ou '''5'''.
==La signification des règles et des axiomes==
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'''==
La logique <math>\mathbb{T}</math> est formée des règles et des axiomes '''K''' et '''T'''. La logique <math>\mathbb{S}\mathbf{4}</math> est <math>\mathbb{T}</math> augmentée de '''4'''. La logique <math>\mathbb{S}\mathbf{5}</math> est <math>\mathbb{S}\mathbf{4}</math> augmentée de '''5'''.
==Les modèles==
Les modèles de la logique épistémique sont des [[sémantique de Kripke|modèles de Kripke]] adaptés spécifiquement aux modalités <math>K_i</math>.
===Présentation intuitive===
L'idée de Kripke est que chaque agent imagine des ''mondes'' dans lesquels telle ou telle proprosition est réalisée et telle ou telle autre ne l'est pas. En fonction du monde où l'agent se trouve, tel autre monde lui paraît ''possible'' ou ''impossible''. Donc pour chaque agent dans un monde donné, certains mondes lui paraissent accessibles à son imagination d'autres pas. La relation qui relie les mondes entre eux est la ''relation d'accessiblité''. Il y a une relation d'accessiblité pour chaque agent. S'il y a ''n'' agents, il y a donc ''n'' relations d'accessiblité étiquettée chacune par le nom de l'agent.
On définit enfin une relation de ''réalisabilité'' entre un monde et une proposition. Un monde ''réalise'' la proposition <math>\varphi</math> siginfiera que la proposition se trouve être «vraie» dans ce monde.
===Présentation formelle===
Dans un <span id-"modèle de Kripke">modèle de Kripke</span>, on distingue:
* un ''univers'' <math>\mathcal{U}</math> dont les éléments notés <math>m</math> sont appélés des ''mondes'',
* pour chaque agent <math>i</math> une relation <math>\equiv_i</math> dite ''relation d'accessibilité'' pour <math>i</math>,
* une relation <math>\Vdash</math> de ''réalisabilité'' entre un monde <math>m</math> et une proposition <math>\varphi</math>, on écrit <math>m\Vdash \varphi</math> et on lit ''<math>m</math> réalise <math>\varphi</math>''.
Un ''cône'' est un ensemble <math>C</math> de mondes (<math>C\subseteq\mathcal{U}</math>) tels
* si <math>m\in C</math>
* et si pour tout <math>i</math> entre <math>1</math> et <math>n</math>, on a <math>m\equiv_i m'</math>,
alors <math>m'\in C</math>.
Une ''intitalisation'' est une application <math>I</math> qui associe à chaque variable un cône de <math>\mathcal{U}</math>.
Le triplet <math>\mathcal{M} = \langle\mathcal{U}_\mathcal{M},\{\equiv_1,...,\equiv_n\}, I_\mathcal{M}\rangle</math> s'appelle un ''modèle'' ou une ''structure de Kripke''. S'il n'y a pas d'ambiguïté on abandonne les indices <math>\mathcal{M}</math>.
La relation de réalisabilité, notée <math>\Vdash_\mathcal{M}</math>, ou <math>\Vdash</math> quand il n'y a pas d'ambiguïté, se définit par induction sur la structure des propositions.
* Si <math>\varphi</math> est une variable <math>x</math>, <math>m\Vdash x</math> si et seulement si <math>m\in I</math>.
* Si <math>\varphi= K_i(\psi)</math>, alors <math>m\Vdash\varphi</math> si et seulement pour tout monde <math>m'\in\mathcal{U}</math> tel que <math>m\equiv_i m'</math> on a <math>m'\Vdash\psi</math>.
* Si <math>\varphi=\varphi_1 \vee \varphi_2</math>, <math>m\Vdash \varphi</math> si et seulement si <math>m\Vdash \varphi_1</math> ou <math>m\Vdash \varphi_2</math>.
* Et ainsi de suite pour chaque connecteur.
On dit que <math>\varphi</math> est valide dans <math>\mathcal{M}</math> ou que <math>\mathcal{M}</math> modélise <math>\varphi</math>, noté <math>\mathcal{M}\vDash\varphi</math>, si pour <math>m\in\mathcal{U}_\mathcal{M}</math>, on a <math>m\Vdash\varphi</math>.
===Validité===
Une proposition <math>\varphi</math> est valide (noté <math>\vDash\varphi</math>) si pour tout modèle <math>\mathcal{M}</math> on a <math>\mathcal{M}\vDash\varphi</math>. Autement dit, une proposition <math>\varphi</math> est valide si pour tout modèle <math>\mathcal{M}</math> et tout monde <math>m</math> dans ce modèle, <math>m\Vdash \varphi</math>.
====Théorème de correction====
Toute proposition ''prouvable'' est ''valide''. Autrement dit, si <math>\vdash\varphi</math> alors <math>\vDash\varphi</math>
===Complétude===
====Complétude de '''T'''====
Si l'on considère les modèles où les relations d'accessibilité sont ''réflexives'' alors toute proposition valide est prouvable dans <math>\mathbb{T}</math>.
====Complétude de '''S4'''====
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 <math>\mathbb{S}_4</math>.
====Complétude de '''S5'''====
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 <math>\mathbb{S}_5</math>.
==Sources==
* J-J Ch. Meyer and 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, and M. Y. Vardi. Reasoning about Knowledge, The MIT Press, 1995. ISBN 0-262-56200-6
[[Catégorie:logique modale]]
[[Catégorie:logique mathématique]]
{{Portail|logique|philosophie}}
[[de:Epistemische Logik]]
[[en:Epistemic logic]]
[[es:Lógica epistémica]]
[[fi:Episteeminen logiikka]]
[[ja:認識論理]]
[[nl:Epistemische logica]]
[[zh:认识逻辑]]