Voir la source de Logique modale

{{sources à lier|date=avril 2015}}
{{Style non encyclopédique|date=avril 2015}}
En [[logique mathématique]], une '''logique modale''' est un type de [[logique formelle]] qui étend la [[logique propositionnelle]], la [[logique du premier ordre]] ou la [[logique d'ordre supérieur]] avec des [[modalité (logique)|modalités]]. Une modalité spécifie des {{ pas clair | qualités du [[valeur de vérité|vrai]] }}. Par exemple, une proposition comme « il pleut » peut être précédée d'une modalité :

* ''Il est nécessaire qu'''il pleuve ;
* ''Demain'', il pleut ;
* ''Christophe Colomb croit qu'''il pleut ;
* ''Il est démontré qu'''il pleut ;
* ''Il est obligatoire qu'''il pleuve.
Il existe une variété de logiques modales comme les [[Logique temporelle|logiques temporelles]], la [[logique épistémique]] (logique de connaissance). En [[informatique]], la logique modale est utilisée pour son expressivité et les aspects [[Algorithmique|algorithmiques]]. Par exemple, la logique temporelle est utilisée pour spécifier des [[Programme informatique|programmes]] puis les [[Vérification de modèles|vérifier]].

== Logique modale aléthique ==
[[Image:Carré aléthique.svg|thumb|Le carré modal : relations entre les modalités de la logique aristotélicienne.]]
En logique modale aléthique (ou aristotélicienne, ou classique), on dégage essentiellement quatre modalités :
* '''[[nécessité|nécessaire]]''' (ce qui ne peut pas ne pas être vrai), noté <math>\Box</math> ;
* '''[[contingence|contingent]]''' (ce qui peut être faux), noté <math>\neg \Box</math> ;
* '''[[possibilité|possible]]''' (ce qui peut être vrai), noté <math>\Diamond</math> ;
* '''[[possibilité|impossible]]''' (ce qui ne peut pas ne pas être faux), noté <math>\neg \Diamond</math>.

Ces 4 modalités sont liées, il suffit d'une pour définir les trois autres.

L'interprétation intuitive (non partagée par l'ensemble de la communauté philosophico-logicienne) est la suivante :
* Nécessaire ≡ impossible pas (<math>\neg \Diamond \neg</math> ≡ <math>\square</math>) ;
* Contingent ≡ possible pas ≡ non nécessaire   ( <math>\Diamond \neg </math> ≡ <math>\neg \square</math>) ;
* Possible ≡ non impossible (<math>\Diamond  </math> ≡ <math>\neg \square \neg </math>).
*Impossible = non possible (<math>\neg\Diamond  </math> ≡ <math>\square \neg</math>).

On distingue donc deux connecteurs unaires duaux l'un de l'autre :
* Le nécessaire <math>\Box</math> ;
* Le possible <math>\Diamond</math>.

<math>\Box</math>p signifie que p est nécessairement vrai, tandis que
<math>\Diamond</math>p signifie que p est possiblement vrai, c'est-à-dire compatible avec les connaissances actuelles.

Exemples :
* <math>\neg \Box</math> trav : il n’est pas nécessaire que les élèves travaillent ;
* <math>\neg \Diamond</math> trav : il n’est pas possible que les élèves travaillent ;
* <math>\Box \neg</math> trav : il est nécessaire que les élèves ne travaillent pas ;
* <math>\Diamond \neg</math> trav : il est possible que les élèves ne travaillent pas.

En logique modale aléthique (ou aristotélicienne, ou classique), nous pouvons exprimer les quatre opérateurs à l’aide d’un seul (ici la nécessité) et de la négation. Ainsi :
* Impossible est <math>\square \neg</math> ;
* Possible est <math>\neg \square \neg</math>.

Une proposition nécessaire ne peut pas être [[Algèbre de Boole (logique)|fausse]] sans impliquer de [[contradiction]], ''a contrario'' d’une proposition ''contingente'' qui peut être fausse sans pour autant impliquer une contradiction.

== Différentes logiques modales ==

D'autres types de logiques modales sont également utilisées, dont les modes sont :
* [[logique épistémique|épistémiques]] (relatifs à la connaissance) :
**'''connu''' par l'agent <math>i</math>, noté <math>C_i</math>
**'''contestable'''
**'''exclu'''
**'''plausible'''
** '''connaissance commune du groupe''' <math>G</math> d'agents, notée <math>CK_G</math>
** '''connaissance partagée du groupe''' <math>G</math> d'agents, notée <math>EK_G</math> (chacun sait)
* [[Logique déontique|déontiques]] (moraux) :
**'''obligatoire''', noté O
**'''interdit''', noté I
**'''permis''', noté P
**'''facultatif''', noté F
* [[logique temporelle|temporels]] :
** '''toujours''', noté <math>\Box</math> ou G
** '''un jour''', noté <math>\Diamond</math>, ou parfois F
** '''jamais''', noté <math>\neg \Diamond</math>
** '''demain''', noté X
** '''jusqu'à ce que''', opérateur binaire noté U
** '''toujours dans le passé''', noté H
** '''un jour passé''', noté P
*[[Logique doxastique|doxastiques]] (sur les croyances) :
**'''cru''', noté B
** '''croyance commune du groupe''' <math>G</math> d'agents, notée <math>CB_G</math>
*[[contrafactuel (philosophique)|contrefactuels]] :
** '''Si A était vrai''', où l'on sait qu'A n'est pas vrai.
* dynamiques (effet d'actions, notées ''a'', sur des propositions) :
**'''Il existe une exécution de''' ''a'' '''telle qu'après''' ''a'', ''p'' '''est vrai''', noté <math>\langle a\rangle p</math>
**''p'' '''est vrai après toute exécution de''' ''a'', noté <math>[a] p</math>.

== Axiomes de logique modale ==

Chaque logique modale est munie d'une série d'[[axiome|axiomes]] qui définissent le fonctionnement des modalités.

On peut ainsi construire différents systèmes en fonction des axiomes admis.

* Le système K conçu par [[Saul Kripke|Kripke]] et appelé système normal ou de Kripke. Il admet les deux axiomes suivants :
** '''(K)''' <math>\Box(A\rightarrow B) \rightarrow( \Box A \rightarrow \Box B)</math> (axiome de distribution de Kripke);
** '''(RN)''' (ou '''(N)''' ou '''(NEC)''') Si <math>A</math> est un théorème, alors <math>\Box A</math> aussi (règle d'inférence de nécessitation).

* Le système D, conçu par l'ajout de l'axiome '''(D)''' au système K :
** '''(D''') <math>\Box P \rightarrow \Diamond P</math> (en logique aristotélicienne, cela exprime que ''la nécessité [[implication (logique)|implique]] la possibilité'').

*Le système T conçu par Robert Feys en 1937 par l'ajout de l'axiome '''(T)''' au système K :
** '''(T)''' (ou '''(M)'''): <math>P \rightarrow \Diamond P</math> (en logique aristotélicienne, cela exprime que ''le fait implique la possibilité'').

* Les systèmes S4 et S5 définis par [[Clarence Irving Lewis]].
** Pour construire S4, on ajoute au système T l'axiome '''(4)''' :
*** '''(4)'''  <math>\Box p\rightarrow\Box\Box p</math>.
** Pour construire S5, on ajoute au système T l'axiome '''(5)''' :
*** '''(5)''' (ou '''(E)''') : <math>\Diamond p\rightarrow\Box\Diamond p</math>.

* Le système B (ou brouwérien), conçu par [[Oskar Becker]] en 1930, par l'ajout de l'axiome '''(B)''' au système T.
** '''(B)''' : <math>p\rightarrow\Box\Diamond p</math>.

On dit qu'un système est plus faible qu'un autre lorsque tout ce qui se démontre dans le premier système se démontre dans le second, mais pas réciproquement.

Ceci hiérarchise, du plus faible au plus fort, les systèmes K, T, S4 et S5. De même, K est plus faible que D et T est plus faible que B.<ref>Jacques-Paul Dubucs, « Logiques non classiques », in ''Encyclopædia universalis'', volume 13, Paris, 1990, {{p.|977-992}}.</ref>

La suite de systèmes K à S5 forme une hiérarchie imbriquée qui compose le noyau de la logique modale normale. L'axiome '''(D)''', quant à lui, est principalement utilisé dans les logiques déontique, doxastique et épistémique.

== Modèles de la logique modale ==

{{Article détaillé|Sémantique de Kripke}}

Les modèles de Kripke, ou modèles de [[mondes possibles]], donnent une sémantique aux logiques modales.
Un modèle de Kripke est la donnée :
* d'un ensemble non vide de mondes possibles <math>W</math> ;
* d'une relation binaire <math>R</math> entre les mondes possibles appelée relation d'accessibilité ;
* d'une valuation <math>V</math> qui donne une valeur de vérité à chaque variable propositionnelle dans chaque monde possible.
La sémantique d'un opérateur modal est définie à partir d'une relation d'accessibilité de la façon suivante : la formule <math>\square A</math> est vraie dans un monde w si, et seulement si la formule <math>A</math> est vraie dans tous les mondes accessibles depuis w par la relation <math>R</math>.

== Classification des systèmes de logique modale ==

Les systèmes de logiques modales sont organisés en fonction des règles d'inférence et des axiomes qui les caractérisent.

=== Logiques modales classiques ===

Les systèmes de logique modale classiques sont ceux qui acceptent la règle d'inférence suivante :

<math>(RE) \frac{A \leftrightarrow B}{\Box A \leftrightarrow \Box B}</math>

L'usage veut que l'on donne à un tel système un nom canonique du type <math>E \xi_1 \xi_2 \cdots \xi_n</math>, où les <math>\xi_i</math> sont les noms des axiomes du systèmes.

=== Logiques modales monotones ===

Les systèmes de logique modale monotones sont ceux qui acceptent la règle d'inférence RM :

<math>(RM) \frac{A \to B}{\Box A \to \Box B}</math>

L'ensemble des systèmes monotones est inclus dans l'ensemble des systèmes classiques.

=== Logiques modales régulières ===

Les systèmes de logique modale réguliers sont ceux qui acceptent la règle d'inférence RR :

<math>(RR) \frac{(A \wedge B) \to C}{(\Box A \wedge \Box B) \to \Box C}</math>

L'ensemble des systèmes réguliers est inclus dans l'ensemble des systèmes monotones.

=== Logiques modales normales ===

Les systèmes de logique modale normaux sont ceux qui acceptent la règle d'inférence RK :

<math>(RK) \frac{(A_1 \wedge \cdots A_n) \to B}{(\Box A_1 \wedge \cdots \Box A_n) \to \Box B}</math>

L'ensemble des systèmes normaux est inclus dans l'ensemble des systèmes réguliers.

Une définition équivalente et plus courante des systèmes normaux est la suivante : un système de logique modal est dit normal s'il comporte l'axiome (K) et accepte la règle de nécessitation (RN) comme règle d'inférence :

<math>(K) \Box (A \to B) \to (\Box A \to \Box B)</math>

<math>(RN) \frac{A}{\Box A}</math>

Les systèmes normaux sont les plus utilisés, car ce sont ceux qui correspondent aux [[Sémantique de Kripke|sémantiques de Kripke]]. Il est cependant possible de trouver des sémantiques pour des logiques classiques non normales, mais elles présentent en général de moins bonnes propriétés.

== Lien avec d'autres logiques ==
La [[logique intuitionniste]] peut être construite sur la logique aléthique comme une logique modale. La logique modale est un fragment de la logique du premier ordre.

== Notes et références ==
{{Références}}

== Voir aussi ==

{{Autres projets
|wiktionary=logique
|wiktionary thésaurus=logique modale/français
}}

=== Articles connexes ===
* [[Contingent]]
* [[Dilemme]]
* [[Fictionnalisme modal]]
* [[Formule de Sahlqvist]]
* [[Logique de la prouvabilité]]
* [[Logique déontique]]
* [[Logiques multi-valuées]]
* [[Preuve ontologique de Gödel]]
* [[Sémantique de Kripke]]
* [[Théorème de Löb]]
* [[Théorie Dezert-Smarandache]]

=== Liens externes ===
* {{en}} James Garson, [http://plato.stanford.edu/entries/logic-modal/ Modal Logic], ''{{Langue|en|The Stanford Encyclopedia of Philosophy}}'', [[Edward N. Zalta]] (ed.), 2007.
* {{en}} {{Langue|en|S4 prover by tableaux method}}, [http://teachinglogic.imag.fr/TableauxS4/ {{Langue|en|S4 prover}}]
* {{en}} Ross Kirsling, [https://github.com/rkirsling/modallogic Modal Logic Playground] 

=== Bibliographie ===
* Patrick Blackburn, Maarten de Rijke et Yde Venema, ''Modal Logic'', Cambridge University Press, 2001
* {{en}} {{Ouvrage|titre=Modal logic, an introduction|ref=Référence:Modal logic, an introduction|auteur=Brian F. Chellas|éditeur=Cambridge University Press|année=1980}}
* L. Fontaine, Logiques modales et anthropologie. [http://www.cairn.info/revue-l-homme-2007-4-page-131.htm Des règles à la parole chez les Indiens yucuna d'Amazonie colombienne]. ''L'Homme'', n.184, 2007, 131-153.
* P. Gochet, P. Gribomont, A. Thayse, Logique, Vol.3 : méthodes pour l'intelligence artificielle, Paris, Hermès-Lavoisier, 2000, 394p. (Résumé très complet en français des principales logiques modale).

{{Palette|Logique|Inférences}}
{{Portail|logique|philosophie|philosophie analytique}}

[[Catégorie:Logique modale]]