Logique modale

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és. Une modalité spécifie des . 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 quil pleut ; Il est démontré qu'''il pleut ; Il est obligatoire quil pleuve. Il existe une variété de logiques modales comme les logiques temporelles, la logique épistémique (logique de connaissance). En informatique, la logique modale est utilisée pour son expressivité et les aspects algorithmiques. Par exemple, la logique temporelle est utilisée pour spécifier des programmes puis les vérifier. En logique modale aléthique (ou aristotélicienne, ou classique), on dégage essentiellement quatre modalités : nécessaire (ce qui ne peut pas ne pas être vrai), noté ; contingent (ce qui peut être faux), noté ; possible (ce qui peut être vrai), noté ; impossible (ce qui ne peut pas ne pas être faux), noté . 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 ( ≡ ) ; Contingent ≡ possible pas ≡ non nécessaire ( ≡ ) ; Possible ≡ non impossible ( ≡ ). Impossible = non possible ( ≡ ). On distingue donc deux connecteurs unaires duaux l'un de l'autre : Le nécessaire ; Le possible . p signifie que p est nécessairement vrai, tandis que p signifie que p est possiblement vrai, c'est-à-dire compatible avec les connaissances actuelles. Exemples : trav : il n’est pas nécessaire que les élèves travaillent ; trav : il n’est pas possible que les élèves travaillent ; trav : il est nécessaire que les élèves ne travaillent pas ; 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.