info

Notes de lecture du livre La logique pas à pas de Jacques Duparc que je paraphrase allégrement.

Logique modale

Syntaxe et sémantique Systèmes logiques Différentes logiques modales


Axiomatique : les systèmes logiques


Nous cherchons l’équivalent en logique modale des tautologies pour le calcul des propositions ; des formules vraies dans tous les modèles, ou plutôt dans toute une classe de modèles car comme on va le voir, la topologie d’un modèle contraint la vérité à l’intérieur de celui-ci.

La logique de la classe C\mathscr{C} est la classe de toutes les formules qui sont valides dans tous les systèmes de transition de C\mathscr{C} : LogC={ϕpour tout SC,Sa,Vϕ}\mathbb{Log}_\mathscr{C}=\set{\phi|\text{pour tout }\mathcal{S}\in\mathscr{C},\mathcal{S}\Vdash^{\forall a,\forall \mathcal{V}} \phi}


Cette logique doit contenir toutes les formules qui sont des tautologies du calcul des propositions puisque ces formule de profondeur modale nulle (pas d’opérateurs modaux) sont nécessairement forcées en tout nœud de n’importe quel modèle.

  • Si la logique contient la formule ϕ\phi, elle doit aussi contenir ϕ\Box\phi. En effet, si ϕ\phi est forcée en tout nœud, alors le successeur de tout nœud force aussi ϕ\phi. On appelle ça la nécessitation (ou généralisation) d'une formule.

  • De plus, si ϕ\phi appartient à la logique, la satisfaction de ϕ\phi en un nœud aa donné est indépendante de la valuation V\mathcal{V} (que PP soit vraie ou fausse, PP est forcée au nœud aa). Par conséquent, que ψ\psi soit vraie ou fausse, la satisfaction de la formule ϕ[ψ/P]\phi[\psi/P] ne varie pas. Toutes substitutions uniformes opérées sur les variables d'une formule appartenant à la logique sera aussi dans la logique.

  • Enfin, la logique de la classe de tous les systèmes de transition est close par modus ponens ; si ϕψ\phi \rightarrow\psi et ψ\psi appartiennent toutes deux à la logique, alors ψ\psi également. En effet, le modus ponens préserve la validité puisque si un modèle vérifie en un noud à la fois ψ\psi et ψϕ\psi\rightarrow\phi, alors (par définition de l'interprétation de l'implication) il vérifie également ϕ\phi.

Pour déterminer des nouvelles tautologies en calcul des propositions, on a utilisé des systèmes de déduction (à la Hilbert, déduction naturelle, calcul des séquents). La modalité complique un peu les choses et seul le système à la Hilbert va pouvoir s’adapter facilement.

  • Un axiome est une formule.
  • Un système formel est un ensemble d'axiomes.

Soient II un ensemble non vide, ϕ\phi une formule et S\text{\bf S} un système formel.
Une preuve de la formule φ\varphi dans le système formel S\text{\bf S} est une suite finie de formule φ1,φ2,,φn\langle\varphi_1,\varphi_2,\ldots,\varphi_n\rangle telle que :

  • φn=ϕ\varphi_n=\phi

  • chaque φl\varphi_l vérifie l'une des quatre conditions suivantes :
    • φlS\varphi_l \in \text{\bf S} (φl\varphi_l est un axiome)
    • φl\varphi_l est obtenue par application de la règle du modus ponens à deux formules d'indice inférieurs φj\varphi_j et φk\varphi_kj,k<lj , k < l (φj=φkφl\varphi_j = \varphi_k\rightarrow\varphi_l)
    • φl=φk[θ/P]\varphi_l = \varphi_k[\theta /P]k<lk < l (substitution d'une variable PP quelconque par une formule θ\theta quelconque dans une formule d'indice inférieure)
    • φl=[i]φj\varphi_l = [i]\varphi_jj<lj < l (φl\varphi_l est obtenue à partir de l'application de la règle de nécessitation appliquée à une formule d'indice inférieure pour une étiquette iIi\in I quelconque)

Exemple 1 :

Si S\text{\bf S} désigne l’ensemble des tautologies du calcul des propositions, alors la suite P(P¬P),Q(Q¬Q),(Q(Q¬Q)),(ϕ(ϕ¬ϕ))\langle P\rightarrow(P\lor\neg P),\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q),\Box (\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q)),\Box (\Diamond \phi\rightarrow(\Diamond \phi\rightarrow\lor\neg\Diamond \phi))\rangle est une preuve de (Q(Q¬Q)),(ϕ(ϕ¬ϕ)\Box (\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q)),\Box (\Diamond \phi\rightarrow(\Diamond \phi\rightarrow\lor\neg\Diamond \phi) dans ce système.

En effet :

  • φ1=P(P¬P)\varphi_1=P\rightarrow(P\lor\neg P) est une tautologie du calcul des propositions et donc un axiome du sydtème formel S\text{\bf S},
  • φ2=Q(Q¬Q)=P(P¬P)[Q/P]\varphi_2 = \Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q) = P\rightarrow(P\lor\neg P)[\Diamond Q /P] est la substitution de la formule Q\Diamond Q à PP dans φ0\varphi_0,
  • φ3=(Q(Q¬Q))\varphi_3 = \Box (\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q)) est obtenu par nécessitation de φ1\varphi_1,
  • φ4=(ϕ(ϕ¬ϕ)=φ3[ϕ/Q]\varphi_4 = \Box (\Diamond \phi\rightarrow(\Diamond \phi\rightarrow\lor\neg\Diamond \phi) = \varphi_3[\phi/Q]

C’est plus élégant de représenter l’enchaînement sous forme d’arbre :

$$ \begin{prooftree} \AxiomC{} \RightLabel{$\scriptsize\;ax$} \UnaryInfC{$P\rightarrow(P\lor\neg P)$} \RightLabel{$\scriptsize\;sub.$} \UnaryInfC{$\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q)$} \RightLabel{$\scriptsize\;nec.$} \UnaryInfC{$\Box (\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q))$} \RightLabel{$\scriptsize\;sub.$} \UnaryInfC{$\Box (\Diamond \phi\rightarrow(\Diamond \phi\rightarrow\lor\neg\Diamond \phi)$} \end{prooftree} $$

Exemple 2 :

Si S\text{\bf S} désigne l’ensemble des tautologies du calcul des propositions auquel on ajoute la formule PPP\rightarrow\Diamond P, alors l’arbre ci-dessous décrit une preuve de (ϕϕ)\Box(\phi\rightarrow\Diamond\Diamond\phi) dans ce système :


Soient S\text{\bf S} un système formel et Γ\Gamma un ensemble de formules appelées hypothèses.
On écrit ΓSϕ\Gamma\vdash_\text{\bf S} \phi s’il existe un ensemble fini de formules {ψ1,ψ2,,ψn}Γ\set{\psi_1,\psi_2,\ldots,\psi_n}\subseteq\Gamma tel que la formule (ψ1ψ2ψn)ϕ(\psi_1\land\psi_2\land\ldots\land\psi_n)\rightarrow\phi puisse être prouvée dans le système formel S\text{\bf S}. Autrement dit le séquent S(ψ1ψ2ψn)ϕ\vdash_\text{\bf S}(\psi_1\land\psi_2\land\ldots\land\psi_n)\rightarrow\phi est vérifiée pour un nombre fini de formules bien choisies de Γ\Gamma.


info

Attention, ici les hypothèses n’ont pas le même sens qu’en logique des propositions. En effet, pour prouver le séquent ϕSψ\phi\vdash_\text{\bf S}\psi, on ne peut pas ajouter ϕ\phi aux axiomes et tenter d’atteindre ψ\psi à partir des règles (modus ponens, substitution uniforme et nécessitation). Il faut ici réussir à prouver la formule ϕψ\phi\rightarrow\psi sur la base des seuls axiomes.

Si on pouvait faire comme en logique des propositions, prouver ϕSϕ\phi\vdash_\text{\bf S}\Box\phi deviendrait évident : on place ϕ\phi dans les axiomes et on applique la règle de nécessitation. Mais non, il faut pouvoir prouver Sϕϕ\vdash_\text{\bf S}\phi\rightarrow\Box\phi et comme on va le voir, dans le système K\text{\bf K}, la formule PPP\rightarrow\Box P n’est pas prouvable (PKPP\nvdash_\text{\bf K}\Box P).


Le système K


Le système K\text{\bf K} est le plus petit système formel qui contient :

  • chaque tautologie du calcul des propositions
  • (K)\text{(K)} : (PQ)(PQ)\Box(P\rightarrow Q)\rightarrow (\Box P\rightarrow \Box Q)
  • (dual)\text{(dual)} : P¬¬P\Diamond P\leftrightarrow\neg\Box\neg P

Le système K\text{\bf K} est minimal en ce sens qu’il est validé dans tout modèle.


Pour tout modèle M=S,V\mathcal{M}=\langle\mathcal{S},\mathcal{V}\rangle et tout nœud aa, si a(PQ)a\Vdash\Box(P\rightarrow Q) et aPa\Vdash\Box P, cela signifie que pour tout nœud bb tel que aba\longrightarrow b, bPQb\Vdash P\rightarrow Q et bPb\Vdash P, par conséquent bQb\Vdash Q et donc aQa\Vdash \Box Q.
Cela montre que l’axiome (K)\text{(K)} est valide dans tous les systèmes de transition.


Pour montrer que PPP\rightarrow\Box P n’est pas prouvable dans K\text{\bf K}, il suffit donc de présenter un modèle (et le système K\text{\bf K} autorise tous les systèmes de transition) où l’implication est fausse pour au moins un nœud. Or on a déjà vu un tel modèle :

Dans ce modèle, on a aPa\Vdash P mais aussi aPa\nVdash \Box P et par conséquent aPPa\nVdash P\rightarrow\Box P.

Cet axiome (K)\text{(K)} (K en l’honneur de Kripke) est appelé axiome de distribution car il permet de distribuer l’opérateur modal \Box à l’intérieur de l’implication. On l’appelle aussi parfois axiome d’omniscience logique car il stipule que si un agent sait que PP implique QQ, alors s’il sait également que PP il doit savoir que QQ. En d’autres termes, l’agent doit connaître toutes les conséquences logiques de ce qu’il sait déjà.

L’axiome (dual)\text{(dual)} permet, lui, de passer d’un opérateur modal à l’autre et est aussi valide dans tout sytème de transition (être sûr de la présence d’un truc revient à ne pas être sûr de son absence, ou pour rester sur la structure du système de transition, dire qu’il existe un chemin vers PP revient à ne pas dire que tous les chemins vont vers ¬P\neg P).
La relation sœur permettant de passer de l’opérateur boite à l’opérateur diamant P¬¬P\Box P \leftrightarrow \neg\Diamond\neg P (si tous les chemins mènent à PP, il n’existe pas de chemin menant à ¬P\neg P) est elle aussi vraie partout.
Ces deux relations soulignent bien la nature duale des opérateurs \Diamond et \Box.

Mais ce système formel n’est pas encore suffisamment riche pour contenir toutes les formules valides dans tous les modèles quels qu’ils soient. Pour cela, il faudrait également considérer toutes les substitutions uniformes possibles (entre autre dans la formule (K)\text{(K)}). On passe alors aux logiques modales.


Logique modale normale


Une logique modale normale L\mathbb{L} est un ensemble de formules qui contient le système formel K\text{\bf K} et qui est clos par :

  • modus ponens $$ \begin{prooftree} \AxiomC{$\phi$} \AxiomC{$\phi\rightarrow\psi$} \RightLabel{$\scriptsize\;mod.p.$} \BinaryInfC{$\psi$} \end{prooftree} $$
  • substitution uniforme $$ \begin{prooftree} \AxiomC{$\phi$} \RightLabel{$\scriptsize\;sub.$} \UnaryInfC{$\phi[\theta/P]$} \end{prooftree} $$
  • nécessitation $$ \begin{prooftree} \AxiomC{$\phi$} \RightLabel{$\scriptsize\;nec.$} \UnaryInfC{$\Box\phi$} \end{prooftree} $$

Toute logique modale normale contient chaque formule ϕ\phi prouvable dans le système formel K\text{\bf K} (si Kϕ\vdash_\text{\bf K}\phi alors ϕ\phi fait partie de toute logique modale normale).

La plus petite logique modale normale est construite sur la base du système formel K\text{\bf K}. On la note LK\mathbb{L}_\text{\bf K}. Le lien entre la logique normale LK\mathbb{L}_\text{\bf K} et le système formel K\text{\bf K} est le suivant : ϕLK\phi \in \mathbb{L}_\text{\bf K} ssi Kϕ\vdash_\text{\bf K}\phi.


Quelques axiomes usuels


(K) :\text{(K) :} (PQ)(PQ)\Box(P\rightarrow Q)\rightarrow(\Box P\rightarrow \Box Q)

On l’a vu, l’axiome (K)\text{(K)} est à la base des logiques modales normales.


(D) :\text{(D) :} PP\Box P\rightarrow \Diamond P

La formule (D)\text{(D)} dit que si quelque chose est nécessaire, alors elle doit être possible. On peut aussi l’interpréter différemment dans d’autres types de logiques que nous allons entrevoir ensuite : en logique déontique, la formule dit que quelque chose d’obligatoire doit être permis ; en logique épistémique, elle dit que si je sais PP, alors il est faux que je sache ¬P\neg P ; et en logique doxastique, que si je crois que PP, alors il est faux que je crois que ¬P\neg P.
(D)\text{(D)} est parfois appelé axiome de consistance.

Comme on l’a vu plus tôt, un système de transition qui valide (D)\text{(D)} n’admet pas d’impasse. Autrement dit, les arcs doivent être non bornés à droite.


(T) :\text{(T) :} PP\Box P\rightarrow P

La formule (T)\text{(T)} dit que si quelque chose est nécessaire, alors elle est. On l’appelle parfois axiome de factivité.
En logique déontique : ce qui est obligatoire est.
En logique épistémique : si je sais PP, alors PP est avéré.
En logique doxastique : si je crois que PP, alors PP est également avéré.

Et nous avons vu qu’un système de transition valide (T)\text{(T)} si et seulement si ce système est réflexif. (T)\text{(T)} est donc aussi l’axiome de réflexivité.


(B) :\text{(B) :} PPP\rightarrow \Box\Diamond P

La formule (B)\text{(B)} dit que si quelque chose est vraie, alors il est nécessaire qu’elle soit possible.
En logique déontique : ce qui est, est obligatoirement permis.
En logique épistémique : si je PP est avéré, alors je sais que je ne sais pas ¬P\neg P.
En logique doxastique : si PP est avéré, alors je crois que je ne crois pas ¬P\neg P.

Et nous avons vu qu’un système de transition valide (B)\text{(B)} si et seulement si ce système est symétrique. (B)\text{(B)} est donc aussi l’axiome de symétrie.


(4) :\text{(4) :} PP\Box P\rightarrow \Box\Box P

La formule (4)\text{(4)} dit que si quelque chose est nécessaire, alors elle est nécessairement nécessaire.
En logique déontique : si quelque chose est obligatoire, c’est obligatoire qu’elle le soit.
En logique épistémique : si je sais PP, alors je sais que je sais PP. Et transitivement, on sait que l’on sait que l’on sait… Autrement dit, avec la formule (4) nous décrivons des agents parfaitement rationnel.
On appelle (4)\text{(4)} l’axiome d’introspection positive dans le cadre de la logique épistémique.

Et nous avons vu qu’un système de transition valide (4)\text{(4)} si et seulement si ce système est transitif. (4)\text{(4)} est donc aussi l’axiome de transitivité.


(5) :\text{(5) :} PP\Diamond P\rightarrow \Box\Diamond P

La formule (5)\text{(5)} dit que s’il n’est pas nécessaire que quelque chose ne soit pas, alors elle est nécessaire.
En logique déontique : si quelque chose est permise, c’est obligatoire qu’elle soit permise.
En logique épistémique : si je ne sais pas quelque chose, alors je sais que je ne le sais pas. L’interprétation épistémique décrit un agent parfaitement conscient de ce qu’il ne sait pas.
En logique doxastique : si je ne crois pas quelsue chose, alors je crois que je ne le crois pas. L’interprétation doxastique décrit un agent parfaitement conscient de ce qu’il ne croit pas.
On appelle (5)\text{(5)} l’axiome d’introspection négative dans le cadre de la logique épistémique.

Et nous avons vu qu’un système de transition valide (5)\text{(5)} si et seulement si ce système est euclidien. (5)\text{(5)} est donc aussi l’axiome d’euclidité.


En prenant ensemble les formules (5)\text{(5)} et (T)\text{(T)}, on regarde des systèmes de transition à la fois euclidiens et réflexifs. Or la conjonction de ces deux propriétés est équivalentes à la conjonction des trois propriétés d’une relation d’équivalence !

Un système de transition est à la fois euclidien et réflexif si et seulement si il est à la fois réflexif, symétrique et transitif.

Autrement dit, un graphe euclidien et réflexif est en fait ni plus ni moins qu’un graphe dans lequel la relation d’accessibilité est une relation d’équivalence (relation définie par les trois propriétés réflexivité, symétrie et transitivité).

  • \Rightarrow :
    • réflexif : c'est immédiat
    • symétrique : si on a un arc aba\longrightarrow b, alors par réflexivité, on a aussi aaa\longrightarrow a, et le caractère euclidien impose donc bab\longrightarrow a.
    • transitif : supposons qu'on ait deux arcs aba\longrightarrow b et bcb\longrightarrow c. Comme on a montré la symétrie du graphe, on a aussi un arc bab\longrightarrow a et le caractère euclidien impose donc un arc aca\longrightarrow c.
  • \Leftarrow :
    • réflexif : c'est immédiat
    • euclidien : supposons qu'on ait deux arcs aba\longrightarrow b et aca\longrightarrow c. La symétrie donne un arc bab\longrightarrow a et la transitivité impose alors un arc bcb\longrightarrow c.



Quelques systèmes formels et logiques usuels


Par la suite, nous confonderons un système formel et la logique qu’il induit par clôture. Les systèmes formels qu’on va introduire sont tous des extensions du système K\text{\bf K}.

  • K\text{\bf K}
  • KD\text{\bf KD} : K{(D)}\text{\bf K}\cup\set{\text{(D)}}
  • KB\text{\bf KB} : K{(B)}\text{\bf K}\cup\set{\text{(B)}}
  • KT\text{\bf KT} : K{(T)}\text{\bf K}\cup\set{\text{(T)}}
  • K4\text{\bf K4} : K{(4)}\text{\bf K}\cup\set{\text{(4)}}
  • KB4\text{\bf KB4} : K{(B),(4)}\text{\bf K}\cup\set{\text{(B),(4)}}
  • KD4\text{\bf KD4} : K{(D),(4)}\text{\bf K}\cup\set{\text{(D),(4)}}
  • KDB\text{\bf KDB} : K{(D),(B)}\text{\bf K}\cup\set{\text{(D),(B)}}
  • KTB\text{\bf KTB} : K{(T),(B)}\text{\bf K}\cup\set{\text{(T),(B)}}
  • S4=KT4\text{\bf S4} = \text{\bf KT4} : K{(T),(4)}\text{\bf K}\cup\set{\text{(T),(4)}}
  • S5=KT5\text{\bf S5} = \text{\bf KT5} : K{(T),(5)}\text{\bf K}\cup\set{\text{(T),(5)}}

Convainquons-nous dans un premier temps que ces axiomes apportent bien quelque chose de plus en montrant par exemple que la logique KB\text{\bf KB} ne permet pas de prouver l’axiome (4)\text{(4)}.

Comme (B)\text{(B)} est vraie dans tout système de transition symétrique, il suffit de trouver un modèle symétrique où au moins un nœud ne satisfait pas (4)=PP\text{(4)}=\Box P\rightarrow\Box\Box P pour montrer que K4⊈KB\text{\bf K4}\not\subseteq \text{\bf KB}.

Comme PP est satisfait dans tout les successeurs de aa, aPa\Vdash\Box P. Mais pour avoir aPa\Vdash\Box\Box P, il faudrait que tous les successeurs de aa satisfassent P\Box P, or ce n'est pas le cas de bb (qui a pour successeur aa lui-même par symétrie et aPa\nVdash P). D'où aPa\nVdash \Box\Box P.

De même, montrons que KTB\text{\bf KTB} ne peut prouver ni (4)\text{(4)} ni (5)\text{(5)}.

(T)\text{(T)} et (B)\text{(B)} seront vraies ensemble dans tout système de transition à la fois réflexif et symétrique. Exhibons un tel modèle où au moins un nœud ne satisfait ni (4)=PP\text{(4)}=\Box P\rightarrow\Box\Box P ni (5)=PP\text{(5)}=\Diamond P\rightarrow\Box\Diamond P.

On constate que dans ce modèle réflexif et symétrique, aa ne satisfait pas (4)\text{(4)} et bb ne satisfait pas une instance de (5)\text{(5)}P=¬QP=\neg Q.

Mais on va préférer dans la suite mettre au jour les inclusions inverses (qui contient qui) grâce à la notion de réduction.

Soient S\text{\bf S} et S’\text{\bf S’} deux systèmes formels et ϕ\phi une formule quelconque,

SS’\text{\bf S}≤\text{\bf S'} si et seulement si SϕS’ϕ\vdash_\text{\bf S}\phi\rightarrow \,\vdash_\text{\bf S'}\phi

Cette relation est réflexive (SS\text{\bf S}≤\text{\bf S}) et transitive (si SS’\text{\bf S}≤\text{\bf S’} et S’S’’\text{\bf S’}≤\text{\bf S’’} alors SS’’\text{\bf S}≤\text{\bf S’’}).

SS’\text{\bf S}≤\text{\bf S’} se lit S\text{\bf S} se réduit à S’\text{\bf S’}. Tout ce qui est prouvé à l’aide de S\text{\bf S} peut également l’être à l’aide de S’\text{\bf S’}.

Si S\text{\bf S} se réduit à S’\text{\bf S’}, cela signifie que S’\text{\bf S’} permet de prouver au moins autant de formules (appelées théorèmes) que S\text{\bf S} et par conséquent, que la classe des systèmes de transition dans lesquels tous les théorèmes de S’\text{\bf S’} sont valides est incluse dans celle des systèmes de transition qui tous valident les théorèmes de S\text{\bf S} (c’est plus dur de raconter plus de choses, ça restreint l’ensemble des modèles possibles).

Autrement dit,

si CS\mathscr{C}_\text{\bf S} et CS’\mathscr{C}_\text{\bf S’} désignent respectivement la classe de tous les systèmes de transition qui valident S\text{\bf S} et S’\text{\bf S’} :

SS’\text{\bf S}≤\text{\bf S'} si et seulement si CS’CS\mathscr{C}_\text{\bf S'}\subseteq\mathscr{C}_\text{\bf S}.


Par contre, les logiques modales normales étant des ensembles de formules satisfaites, pour elles l’inclusion est dans l’autre sens :

Lorsque S\text{\bf S} et S’\text{\bf S’} contiennent tous les deux le système formel K\text{\bf K}, les logiques modales normales qu’ils engendrent (LS\mathbb{L}_\text{\bf S} et LS’\mathbb{L}_\text{\bf S’}) vérifient la relation suivante :

SS’\text{\bf S}≤\text{\bf S'} si et seulement si LSLS’\mathbb{L}_\text{\bf S}\subseteq\mathbb{L}_\text{\bf S'}.

On obtient alors immédiatement les réductions suivantes :

  • KK4\text{\bf K}≤\text{\bf K4}
  • KKB\text{\bf K}≤\text{\bf KB}
  • KKD\text{\bf K}≤\text{\bf KD}
  • K4KB4\text{\bf K4}≤\text{\bf KB4}
  • K4KD4\text{\bf K4}≤\text{\bf KD4}
  • KBKB4\text{\bf KB}≤\text{\bf KB4}
  • KBKDB\text{\bf KB}≤\text{\bf KDB}
  • KDKDB\text{\bf KD}≤\text{\bf KDB}
  • KDKD4\text{\bf KD}≤\text{\bf KD4}
  • KTKTB\text{\bf KT}≤\text{\bf KTB}
  • KTKT4\text{\bf KT}≤\text{\bf KT4}

Montrons maintenant que :

KDKT\text{\bf KD}≤\text{\bf KT}


Il suffit de montrer que la formule (D)\text{(D)} peut être prouvée grâce au système KT\text{\bf KT}, c’est-à-dire : KTPP\vdash_\text{\bf KT} \Box P\rightarrow\Diamond P.

On en déduit immédiatement :

  • KDBKTB\text{\bf KDB}≤\text{\bf KTB}
  • KD4KT4=S4\text{\bf KD4}≤\text{\bf KT4=S4}

On peut aussi montrer que :

KTBS5\text{\bf KTB}≤\text{\bf S5}


Il suffit de montrer que la formule (B)\text{(B)} peut être prouvée grâce au système KT5\text{\bf KT5}, c’est-à-dire : S5PP\vdash_\text{\bf S5} P\rightarrow\Box\Diamond P.

Montrons d’abord que KTPP\vdash_\text{\bf KT}P\rightarrow\Diamond P, ce qui montre également que KT5PP\vdash_\text{\bf KT5}P\rightarrow\Diamond P.

Puis utilisons ce résultat pour montrer que S5PP\vdash_\text{\bf S5}P\rightarrow\Box\Diamond P

S4S5\text{\bf S4}≤\text{\bf S5}


Il suffit de montrer que la formule (4)\text{(4)} peut être prouvée grâce au système KT5\text{\bf KT5}, c’est-à-dire : S5PP\vdash_\text{\bf S5} \Box P\rightarrow\Box\Box P.

On commence par montrer S5PP\vdash_\text{\bf S5} \Box P\rightarrow\Box\Diamond\Box P en ajoutant juste une substitution au théorème précédant :

$$ \begin{prooftree} \AxiomC{} \RightLabel{$\scriptsize\;th.$} \UnaryInfC{$ P\rightarrow\Box\Diamond P$} \RightLabel{$\scriptsize\;sub.$} \UnaryInfC{$ \Box P \rightarrow \Box\Diamond \Box P$} \end{prooftree} $$
On montre ensuite S5PP\vdash_\text{\bf S5} \Diamond\Box P\rightarrow \Box P
Puis on montre S5PP\vdash_\text{\bf S5} \Box\Diamond\Box P\rightarrow \Box\Box P
Pour enfin pouvoir conclure :

KB4S5\text{\bf KB4}≤\text{\bf S5}


Il faut montrer à la fois que :

  • la formule (4)\text{(4)} peut être prouvée dans le système S5\text{\bf S5} et on l'a fait dans la démonstration de la réduction de S4\text{\bf S4} à S5\text{\bf S5},
  • la formule (B)\text{(B)} peut être prouvée dans le système S5\text{\bf S5} et on l'a fait dans la démonstration de la réduction de KTB\text{\bf KTB} à S5\text{\bf S5},

Représentons tout ça graphiquement en utilisant le code suivant : une flèche allant de S\text{\bf S} à S’\text{\bf S’} signifie que la relation SS’\text{\bf S}≤\text{\bf S’} est avérée (S\text{\bf S} se réduit à S’\text{\bf S’}).

Et comme on l’a vu, la réduction d’un système formel à un autre implique l’inclusion inverse entre les classes de tous les systèmes de transition qui valident ces systèmes formels.
Dans le graphique suivant, une flèche allant de C\mathscr{C} à C\mathscr{C’} désigne donc l’inclusion inverse CC\mathscr{C}\supseteq\mathscr{C’}.

Le projet est maintenant de préciser le rapport entre axiomatique et sémantique avec l’espoir que l’ensemble des formules valides sur les structures d’un certain type soit identique à l’ensemble des axiomes et théorèmes d’un certain système (ce qu’on a appelé une logique modale), car ainsi la validité formera une interprétation du système. Mais pour s’assurer de cette adéquation entre sémantique et axiomatique, il faut d’une part obtenir la correction (ou solidité, soundness en anglais) du système (toutes les formules prouvables sont vraies), et sa réciproque, la complétude (toutes les formules vraies sont prouvables).
Dit autrement, on doit pouvoir déduire du système formel tout le vrai (complétude) et rien que le vrai (correction).


On va d’abord chercher à faire correspondre une logique modale normale à chaque classe de systèmes de transitions.

Soit C\mathscr{C} une classe de systèmes de transition et L\mathbb{L} une logique modale normale, L\mathbb{L} est correcte par rapport à la classe C\mathscr{C} (noté C\mathscr{C}-correcte) si pour toute formule ϕ\phi et pour tout système de transition S\mathcal{S} de la classe C\mathscr{C}, si Lϕ\vdash_\mathbb{L}\phi alors Sa,Vϕ\mathcal{S}\Vdash^{\forall a,\forall \mathcal{V}}\phi.
Ce qu’on peut aussi écrire :
si Lϕ alors Cϕ\text{si } \vdash_\mathbb{L}\phi \text{ alors }\models_{\mathscr{C}}\phi

À chacune des onze classes, on peut faire correspondre une logique modale normale qui se trouve être correcte pour cette classe.

  • si Kϕ\vdash_\text{\bf K}\phi alors Cϕ\models_{\mathscr{C}}\phi
  • si K4ϕ\vdash_\text{\bf K4}\phi alors Ctr.ϕ\models_{\mathscr{C}_{tr.}}\phi
  • si KDϕ\vdash_\text{\bf KD}\phi alors Cn.b.d.ϕ\models_{\mathscr{C}_{n.b.d.}}\phi
  • si KD4ϕ\vdash_\text{\bf KD4}\phi alors Ctr.,n.b.d.ϕ\models_{\mathscr{C}_{tr.,n.b.d.}}\phi
  • si KTϕ\vdash_\text{\bf KT}\phi alors Cref.ϕ\models_{\mathscr{C}_{ref.}}\phi
  • si S4ϕ\vdash_\text{\bf S4}\phi alors Cref.,tr.ϕ\models_{\mathscr{C}_{ref.,tr.}}\phi
  • si KBϕ\vdash_\text{\bf KB}\phi alors Csym.ϕ\models_{\mathscr{C}_{sym.}}\phi
  • si KB4ϕ\vdash_\text{\bf KB4}\phi alors Csym.,tr.ϕ\models_{\mathscr{C}_{sym.,tr.}}\phi
  • si KDBϕ\vdash_\text{\bf KDB}\phi alors Csym.,n.b.d.ϕ\models_{\mathscr{C}_{sym.,n.b.d.}}\phi
  • si KTBϕ\vdash_\text{\bf KTB}\phi alors Cref.,sym.ϕ\models_{\mathscr{C}_{ref.,sym.}}\phi
  • si S5ϕ\vdash_\text{\bf S5}\phi alors Cref.,sym.,tr.ϕ\models_{\mathscr{C}_{ref.,sym.,tr.}}\phi

On a déjà en fait déjà tout démontré.
En effet, on a montré que les axiomes de la logique normale minimale (tautologies du calcul des propositions, (K)\text{(K)} et (dual)\text{(dual)}) sont satisfaites en tout nœud et pour toute valuation de tous les systèmes de transitions. Et on a montré que les trois opérations utilisés pour les preuves (la nécéssitation, la substitution uniforme et le modus ponens) préservent la validité. Donc une formule prouvable dans K\text{\bf K} est valide dans tout système de transition ( K\text{\bf K} est C\mathscr{C}-correcte).

Ensuite, on a montré que chacun des axiomes modaux supplémentaires ajoutés à K\text{\bf K} pour obtenir les autres logiques normales ont une validité limitée à une classe spécifique de systèmes de transition.

  • (T)\text{(T)} est valide dans tout système de transition réflexif.
  • (B)\text{(B)} est valide dans tout système de transition symétrique.
  • (4)\text{(4)} est valide dans tout système de transition transitif.
  • (D)\text{(D)} est valide dans tout système de transition non borné à droite.
  • (4)\text{(4)} est valide dans tout système de transition euclidien.

Et on a montré qu’un graphe est à la fois réflexif et euclidien si et seulement si il est réflexif, symétrique et transitif.

On représente graphiquement par une flèche “XCx\text{\bf X}\longrightarrow\mathscr{C}_x” la relation de correction : “si Xϕ\vdash_\text{\bf X}\phi, alors Cxϕ\models_{\mathscr{C}_x}\phi”.

On va essayer maintenant d’associer les classe aux logiques, la sémantique à la syntaxe.

Soit C\mathscr{C} une classe de systèmes de transition et L\mathbb{L} une logique modale normale.

  • L\mathbb{L} est faiblement complète par rapport à la classe C\mathscr{C} (noté C\mathscr{C}-faiblement complète) si pour toute formule ϕ\phi :
    si Cϕ alors Lϕ\text{si }\models_\mathscr{C}\phi \text{ alors } \vdash_\mathbb{L}\phi
  • L\mathbb{L} est fortement complète par rapport à la classe C\mathscr{C} (noté C\mathscr{C}-fortement complète) si pour toute formule ϕ\phi et tout ensemble de formules Γ\Gamma :
    si ΓCϕ alors ΓLϕ\text{si } \Gamma \models_\mathscr{C}\phi \text{ alors } \Gamma \vdash_\mathbb{L}\phi

On a alors le théorème de forte complétude suivant :

  1. si ΓCϕ\Gamma\models_{\mathscr{C}}\phi alors ΓKϕ\Gamma\vdash_\text{\bf K}\phi
  2. si ΓCtr.ϕ\Gamma\models_{\mathscr{C}_{tr.}}\phi alors ΓK4ϕ\Gamma\vdash_\text{\bf K4}\phi
  3. si ΓCn.b.d.ϕ\Gamma\models_{\mathscr{C}_{n.b.d.}}\phi alors ΓKDϕ\Gamma\vdash_\text{\bf KD}\phi
  4. si ΓCtr.,n.b.d.ϕ\Gamma\models_{\mathscr{C}_{tr.,n.b.d.}}\phi alors ΓKD4ϕ\Gamma\vdash_\text{\bf KD4}\phi
  5. si ΓCref.ϕ\Gamma\models_{\mathscr{C}_{ref.}}\phi alors ΓKTϕ\Gamma\vdash_\text{\bf KT}\phi
  6. si ΓCref.,tr.ϕ\Gamma\models_{\mathscr{C}_{ref.,tr.}}\phi alors ΓS4ϕ\Gamma\vdash_\text{\bf S4}\phi
  7. si ΓCsym.ϕ\Gamma\models_{\mathscr{C}_{sym.}}\phi alors ΓKBϕ\Gamma\vdash_\text{\bf KB}\phi
  8. si ΓCsym.,tr.ϕ\Gamma\models_{\mathscr{C}_{sym.,tr.}}\phi alors ΓKB4ϕ\Gamma\vdash_\text{\bf KB4}\phi
  9. si ΓCsym.,n.b.d.ϕ\Gamma\models_{\mathscr{C}_{sym.,n.b.d.}}\phi alors ΓKDBϕ\Gamma\vdash_\text{\bf KDB}\phi
  10. si ΓCref.,sym.ϕ\Gamma\models_{\mathscr{C}_{ref.,sym.}}\phi alors ΓKTBϕ\Gamma\vdash_\text{\bf KTB}\phi
  11. si ΓCref.,sym.,tr.ϕ\Gamma\models_{\mathscr{C}_{ref.,sym.,tr.}}\phi alors ΓS5ϕ\Gamma\vdash_\text{\bf S5}\phi

Pour le démontrer on va avoir besoin de nouvelles définitions et de plusieurs lemmes.

Soient S\text{\bf S} un système formel et Γ\Gamma un ensemble de formules,

Γ\Gamma est S\text{\bf S}-consistant si et seulement si ΓS\Gamma\nvdash_\text{\bf S}\bot.

Dans le cas contraire, Γ\Gamma est dit S\text{\bf S}-inconsistant.

Lemme d'existence

Soient C\mathscr{C} une classe de système de transition et L\mathbb{L} une logique modale normale,

L\mathbb{L} est C\mathscr{C}-(fortement) complète si et seulement si pour tout ΓL\Gamma\subseteq\mathbb{L} qui est L\mathbb{L}-consistant, il existe SC,V\mathcal{S}\in\mathscr{C},\mathcal{V} et aa tels que S,V,aΓ\langle\mathcal{S},\mathcal{V},a\rangle\Vdash\Gamma.


  • \Rightarrow :
    puisque L\mathbb{L} est C\mathscr{C}-complète, un ensemble de formules quelconque L\mathbb{L}-consistant ΓL\Gamma\subseteq\mathbb{L} est nécessairement satisfaisable pour un système de transition de la classe C\mathscr{C}. En effet, si ce n'était pas le cas, l'expression ΓC\Gamma\models_\mathscr{C}\bot serait vraie, mais alors nous pourrions en déduire ΓL\Gamma\vdash_\mathbb{L}\bot en utilisant la C\mathscr{C}-complétude de L\mathbb{L}.
  • \Leftarrow :
    montrons la contraposée. On suppose donc que L\mathbb{L} n'est pas C\mathscr{C}-complète. Soit donc Γ\Gamma un ensemble de formules et ϕ\phi une formule tels que ΓCϕ\Gamma\models_\mathscr{C}\phi mais ΓLϕ\Gamma\nvdash_\mathbb{L}\phi. Il apparaît dès lors que Γ{¬ϕ}L\Gamma\cup\set{\neg\phi}\nvdash_\mathbb{L}\bot est vérifiée, car Γ{¬ϕ}L\Gamma\cup\set{\neg\phi}\vdash_\mathbb{L}\bot entraînerait ΓL¬ϕ\Gamma\vdash_\mathbb{L}\neg\phi\rightarrow\bot puis, en passant par la contraposée, ΓLϕ\Gamma\vdash_\mathbb{L}\phi. Par conséquent Γ{¬ϕ}\Gamma\cup\set{\neg\phi} est L\mathbb{L}-consistant et pourtant, pour tout système de transition SC\mathcal{S}\in\mathscr{C}, V\mathcal{V} et aa, S,V,aΓ{¬ϕ}\langle\mathcal{S},\mathcal{V},a\rangle\nVdash\Gamma\cup\set{\neg\phi}.

L’idée pour démontrer la complétude est de chercher un modèle S,V\langle\mathcal{S},\mathcal{V}\rangle dont le système de transition fait partie de la classe considérée et un nœud aa tels que S,V,aΓ\langle\mathcal{S},\mathcal{V},a\rangle\Vdash\GammaΓ\Gamma est un ensemble de formules L\mathbb{L}-consistant.
On va mettre au point un tel modèle en modelant les nœuds de son système de distribution directement à partir d’ensembles de formules ! La sémantique détourne ainsi la syntaxe à son profit en donnant vie à une sorte de Golem syntaxique.


Soient L\mathbb{L} une logique modale normale et Γ\Gamma un ensemble de formules,

Γ\Gamma est maximal L\mathbb{L}-consistant (MC) si et seulement si ΓL\Gamma\nvdash_\mathbb{L}\bot et pour tout ensemble ΓΓ\Gamma \subsetneq \Gamma', ΓL\Gamma'\vdash_\mathbb{L}\bot.

Remarques :

si Γ\Gamma est maximal L\mathbb{L}-consistant, alors :

  • LΓ\mathbb{L}\subseteq\Gamma
  • Γ\Gamma est clos par modus ponens
  • pour toute formule ϕ\phi, ϕΓ\phi\in\Gamma ou ¬ϕΓ\neg\phi\in\Gamma
  • pour toutes formules ϕ\phi et ψ\psi, ϕψΓ\phi\lor\psi\in\Gamma si et seulement si ϕΓ\phi\in\Gamma ou ψΓ\psi\in\Gamma
Lemme de Lindenbaum

Si Γ\Gamma est L\mathbb{L}-consistant, alors il existe Γmax\Gamma_{max} maximal L\mathbb{L}-consistant tel que ΓΓmax\Gamma\subseteq\Gamma_{max}.


Soit (ϕn)nN(\phi_n)_{n\in\mathbb{N}} une énumération de toutes les formules. On définit :

  • Γ0=Γ\Gamma_0=\Gamma
  • Γn+1={Γn{ϕn} si Γn{ϕn}LΓn{¬ϕn} sinon\Gamma_{n+1}=\begin{cases}\Gamma_n\cup\set{\phi_n} \text{ si } \Gamma_n\cup\set{\phi_n}\nvdash_\mathbb{L}\bot\\ \Gamma_n\cup\set{\neg\phi_n} \text{ sinon}\end{cases}
  • Γmax=nNΓn\displaystyle \Gamma_{max}=\bigcup_{n\in\mathbb{N}}\Gamma_n
Γmax\Gamma_{max} est L\mathbb{L}-consistant car sinon il existerait un plus petit entier nn tel que Γn+1L\Gamma_{n+1}\vdash_\mathbb{L}\bot. Nous aurions alors Γn{ϕn}L\Gamma_n\cup\set{\phi_n}\vdash_\mathbb{L}\bot et Γn{¬ϕn}L\Gamma_n\cup\set{\neg\phi_n}\vdash_\mathbb{L}\bot par construction de Γmax\Gamma_{max}. En utilisant le raisonnement par l'absurde, nous obtenons à la fois ΓnLϕn\Gamma_n\vdash_\mathbb{L}\phi_n et ΓnL¬ϕn\Gamma_n\vdash_\mathbb{L}\neg\phi_n, ce qui entraîne ΓnL\Gamma_n\vdash_\mathbb{L}\bot, contredisant la fait que par minimalité de l'entier nn, Γn\Gamma_n est L\mathbb{L}-consistant.

Γmax\Gamma_{max} est maximal car sinon il existerait Γ\Gamma’ L\mathbb{L}-consistant tel que ΓmaxΓ\Gamma_{max}\subsetneq\Gamma’. Dans ce cas, une formule quelconque ψ\psi telle que ψΓΓmax\psi\in\Gamma’\setminus\Gamma_{max} apparaîtrait dans l’énumération (ϕn)nN(\phi_n)_{n\in\mathbb{N}} de toutes les formules et il existerait ainsi un entier nn tel que ψ=ϕn\psi=\phi_n. Par construction de Γmax\Gamma_{max}, comme ϕn∉Γmax\phi_n\not\in\Gamma_{max}, Γn{ϕn}L\Gamma_n\cup\set{\phi_n}\vdash_\mathbb{L}\bot est vérifiée. Donc Γmax{ϕn}L\Gamma_{max}\cup\set{\phi_n}\vdash_\mathbb{L}\bot ce qui entraîne ΓL\Gamma’\vdash_\mathbb{L}\bot, contredisant la L\mathbb{L}-consistance de Γ\Gamma’.


Soit L\mathbb{L} une logique modale normale, le modèle canonique ML\mathcal{M}_\mathbb{L} est défini par ML=NL,AL,VL\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle avec :

  • NL={ΓΓ maximal L-consistant}N_\mathbb{L}=\set{\Gamma|\Gamma\text{ maximal }\mathbb{L}\text{-consistant}}
  • ALA_\mathbb{L} défini par ΓΓ\Gamma\longrightarrow\Gamma' si et seulement si pour toute formule ϕ\phi, si ϕΓ\phi\in\Gamma' alors ϕΓ\Diamond\phi\in\Gamma (c.-à-d. Γ{ϕ:ϕΓ}\Gamma\supseteq\set{\Diamond\phi : \phi\in\Gamma'})
  • VL\mathcal{V}_\mathbb{L} est défini par VL(P)={ΓNLPΓ}\mathcal{V}_\mathbb{L}(P)=\set{\Gamma\in\N_\mathbb{L}|P\in\Gamma} (c.-à-d. ΓP\Gamma\Vdash P si et seulement si PΓP\in\Gamma)

Lemme (\longrightarrow et \Box)

Soit L\mathbb{L} une logique modale normale et ML=NL,AL,VL\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle le modèle canonique associé à L\mathbb{L}. Pour tout nœud Γ,ΓNL\Gamma,\Gamma’\in N_\mathbb{L}, on a :

ΓΓ\Gamma\longrightarrow\Gamma' si et seulement si pour toute formule ϕ\phi, si ϕΓ\Box\phi\in\Gamma alors ϕΓ\phi\in\Gamma'.


  • \Rightarrow :
    Raisonnons par l'absurde en supposant ϕΓ\Box\phi\in\Gamma et ϕ∉Γ\phi\not\in\Gamma'. Par maximale L\mathbb{L}-consistance de Γ\Gamma', ¬ϕΓ\neg\phi\in\Gamma'. Par définition de l'arc ΓΓ\Gamma\longrightarrow\Gamma', ¬ϕΓ\Diamond\neg\phi\in\Gamma et puisque Γ\Gamma est consistant, ¬¬ϕ∉Γ\neg\Diamond\neg\phi\not\in\Gamma, d'où ϕ∉Γ\Box\phi\not\in\Gamma (où on a utilisé la dualité entre \Diamond et \Box). Contradiction.
  • \Leftarrow :
    Soit ϕΓ\phi\in\Gamma'. Raisonnons par l'absurde en supposant ϕ∉Γ\Diamond\phi\not\in\Gamma (ce qui signifie que Γ  ̸ ⁣ ⁣Γ\Gamma\,\,\not\!\!\longrightarrow\Gamma'). Alors par maximale L\mathbb{L}-consistance ¬ϕΓ\neg\Diamond\phi\in\Gamma, par conséquent ¬¬¬ϕΓ\neg\Diamond\neg\neg\phi\in\Gamma et donc ¬ϕΓ\Box\neg\phi\in\Gamma (où on a utilisé la dualité entre \Diamond et \Box). Par hypothèse, ¬ϕΓ\Box\neg\phi\in\Gamma entraîne ¬ϕΓ\neg\phi\in\Gamma', ce qui contredit la L\mathbb{L}-consistance de Γ\Gamma'.

Lemme (\longrightarrow et \Diamond)

Soit L\mathbb{L} une logique modale normale et ML=NL,AL,VL\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle le modèle canonique associé à L\mathbb{L}. Pour tout nœud Γ,ΓNL\Gamma,\Gamma’\in N_\mathbb{L} :

Si ϕΓ\Diamond\phi\in\Gamma alors il existe Γ\Gamma' tel que ΓΓ\Gamma\longrightarrow\Gamma' et ϕΓ\phi\in\Gamma'.


Supposons ϕΓ\Diamond\phi\in\Gamma. Pour obtenir Γ\Gamma’, on construit d’abord Θ={ϕ}{ψψΓ}\Theta=\set{\phi}\cup\set{\psi|\Box\psi\in\Gamma}. Cet ensemble est consistant car sinon il existerait ψ1,,ψkΘ\psi_1,\ldots,\psi_k\in\Theta tels que L(ψ1ψk)¬ϕ\vdash_\mathbb{L}(\psi_1\land\ldots\land\psi_k)\rightarrow\neg\phi. Par nécessitation, L((ψ1ψk)¬ϕ)\vdash_\mathbb{L}\Box((\psi_1\land\ldots\land\psi_k)\rightarrow\neg\phi). Et par distributivité (utilisation de l’axiome (K)\text{(K)}) L(ψ1ψk)¬ϕ\vdash_\mathbb{L}\Box(\psi_1\land\ldots\land\psi_k)\rightarrow\Box\neg\phi. Et puisque dans toute logique normale L(ψ1ψk)(ψ1ψk)\vdash_\mathbb{L}(\Box\psi_1\land\ldots\land\Box\psi_k)\rightarrow\Box(\psi_1\land\ldots\land\psi_k), on obtient finalement L(ψ1ψk)¬ϕ\vdash_\mathbb{L}(\Box\psi_1\land\ldots\land\Box\psi_k)\rightarrow\Box\neg\phi. Par conséquent ΓL¬ϕ\Gamma\vdash_\mathbb{L}\Box\neg\phi, ce qui implique que ¬ϕΓ\Box\neg\phi\in\Gamma par maximalité, et donc également ¬ϕΓ\neg\Diamond\phi\in\Gamma (par dualité). Or par hypothèse, ϕΓ\Diamond\phi\in\Gamma, ce qui entraîne l’inconsistance de Γ\Gamma. Contradiction.
Comme on vient de montrer que l’ensemble Θ={ϕ}{ψψΓ}\Theta=\set{\phi}\cup\set{\psi|\Box\psi\in\Gamma} est L\mathbb{L}-consistant, il suffit de prendre pour Γ\Gamma’ l’ensemble Θmax\Theta_{max} maximal L\mathbb{L}-consistant donné par le lemme de Lindenbaum tel que ΘΘmax\Theta\subseteq\Theta_{max}. On a bien ainsi un nœud de NLN_\mathbb{L} contenant ϕ\phi.


Lemme de vérité

Soit L\mathbb{L} une logique modale normale et ML=NL,AL,VL\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle le modèle canonique associé à L\mathbb{L}. Pour tout nœud ΓNL\Gamma\in N_\mathbb{L} :

ML,Γϕ\langle\mathcal{M}_\mathbb{L},\Gamma\rangle\Vdash\phi si et seulement si ϕΓ\phi\in\Gamma


La démonstration se fait par induction sur la hauteur de la formule ϕ\phi.

  • si ht(ϕ)=0ht(\phi)=0, alors ϕ=\phi=\top ou ϕ=\phi=\bot ou ϕ\phi est une variable propositionnelle et Γϕ\Gamma\Vdash\phi ssi ϕΓ\phi\in\Gamma est la définition même de la valuation VL\mathcal{V}_\mathbb{L}.
  • si ht(ϕ)=n+1ht(\phi)=n+1
    • si ϕ=¬ψ\phi=\neg\psi, alors Γ¬ϕ\Gamma\Vdash\neg\phi ssi Γψ\Gamma\nVdash\psi. Or par hypothèse d'induction Γψ\Gamma\nVdash\psi ssi ψ∉Γ\psi\not\in\Gamma. Par maximalité de Γ\Gamma, on obtient ¬ψΓ\neg\psi\in\Gamma.
    • si ϕ=(ψ1ψ2)\phi=(\psi_1\lor\psi_2), alors Γ(ψ1ψ2)\Gamma\Vdash(\psi_1\lor\psi_2) ssi Γψ1\Gamma\Vdash\psi_1 ou Γψ2\Gamma\Vdash\psi_2.
      Par hypothèse d'induction, Γψ1\Gamma\Vdash\psi_1 ssi ψ1Γ\psi_1\in\Gamma et Γψ2\Gamma\Vdash\psi_2 ssi ψ2Γ\psi_2\in\Gamma. Et par maximalité de Γ\Gamma, ψ1Γ\psi_1\in\Gamma ou ψ2Γ\psi_2\in\Gamma ssi (ψ1ψ2)Γ(\psi_1\lor\psi_2)\in\Gamma.
    • si ϕ=(ψ1ψ2)\phi=(\psi_1\land\psi_2), alors Γ(ψ1ψ2)\Gamma\Vdash(\psi_1\lor\psi_2) ssi Γψ1\Gamma\Vdash\psi_1 et Γψ2\Gamma\Vdash\psi_2.
      Par hypothèse d'induction, Γψ1\Gamma\Vdash\psi_1 ssi ψ1Γ\psi_1\in\Gamma et Γψ2\Gamma\Vdash\psi_2 ssi ψ2Γ\psi_2\in\Gamma. Or par L\mathbb{L}-consistance, ψ1Γ\psi_1\in\Gamma et ψ2Γ\psi_2\in\Gamma ssi (ψ1ψ2)Γ(\psi_1\land\psi_2)\in\Gamma.
    • si ϕ=(ψ1ψ2)\phi=(\psi_1\rightarrow\psi_2). On déduit ce cas de ¬ψ1ψ2\neg\psi_1\lor\psi_2.
    • si ϕ=(ψ1ψ2)\phi=(\psi_1\leftrightarrow\psi_2). On déduit ce cas de (ψ1ψ2)(ψ2ψ1)(\psi_1\rightarrow\psi_2)\land(\psi_2\rightarrow\psi_1).
    • si ϕ=ψ\phi=\Diamond\psi, alors Γψ\Gamma\Vdash\Diamond \psi ssi il existe Γ,ΓΓ\Gamma',\Gamma\longrightarrow\Gamma' et Γψ\Gamma'\Vdash\psi. Or par hypothèse d'induction Γψ\Gamma'\Vdash\psi ssi ψΓ\psi\in\Gamma'. Finalement, par définition de la relation ΓΓ\Gamma\longrightarrow\Gamma' et par le lemme (\longrightarrow et \Diamond) ψΓ\psi\in\Gamma' ssi ψΓ\Diamond\psi\in\Gamma.
    • si ϕ=ψ\phi=\Box\psi, alors Γϕ\Gamma\Vdash\Box\phi ssi Γ¬¬ψ\Gamma\Vdash\neg\Diamond\neg\psi ssi ¬¬ψΓ\neg\Diamond\neg\psi\in\Gamma ssi ψΓ\Box\psi\in\Gamma (par maximal L\mathbb{L}-consistance).

Nous voilà parés pour démontrer la complétude forte des onze logiques normales décrites grâce au modèle canonique de chacune.

Le lemme d’existence nous dit que L\mathbb{L} est C\mathscr{C}-fortement complète ssi pour tout ΓL\Gamma\subseteq\mathbb{L}, L\mathbb{L}-consistant, il existe SC\mathcal{S}\in\mathscr{C}, V\mathcal{V} et aa tels que S,V,aΓ\langle\mathcal{S},\mathcal{V},a\rangle\Vdash\Gamma.

Pour chaque logique normale, nous allons choisir le modèle canonique ML=NL,AL,VL\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle associé. Et pour le nœud aa, nous allons prendre Γmax\Gamma_{max}. Le lemme de vérité nous dit alors que ML,Γmaxϕ\langle\mathcal{M}_\mathbb{L},\Gamma_{max}\rangle\Vdash\phi ssi ϕΓmax\phi\in\Gamma_{max}. En conséquence, puisque ΓΓmax\Gamma\subseteq\Gamma_{max}, il ressort que ML,ΓmaxΓ\langle\mathcal{M}_\mathbb{L},\Gamma_{max}\rangle\Vdash\Gamma.

Il ne reste plus qu’à vérifier à chaque fois que le modèle canonique est bien construit sur la base d’un système de transition de la classe C\mathscr{C} considérée.

  1. MKC\mathcal{M}_\text{\bf K}\in\mathscr{C} : comme C\mathscr{C} désigne la classe de tous les systèmes de transition, il n'ya rien à montrer.
  2. MK4Ctr.\mathcal{M}_\text{\bf K4}\in\mathscr{C}_{tr.} :
    il faut montrer que pour tout nœud Ξ1\Xi_1, Ξ2\Xi_2 et Ξ3\Xi_3 de MK4\mathcal{M}_\text{\bf K4}, si Ξ1Ξ2\Xi_1\longrightarrow \Xi_2 et Ξ2Ξ3\Xi_2\longrightarrow \Xi_3, alors Ξ1Ξ3\Xi_1\longrightarrow \Xi_3.
    La formule (4)=pP\text{(4)}=\Box p\rightarrow\Box\Box P est équivalente (par dualité) à la formule ¬¬P¬¬¬¬P\neg\Diamond\neg P\rightarrow\neg\Diamond\neg\neg\Diamond\neg P elle même équivalente à ¬P¬P\Diamond\Diamond\neg P\rightarrow\Diamond\neg P (en passant par la contraposée et en éliminant les doubles négations). Comme ¬P¬PΓ\Diamond\Diamond\neg P\rightarrow\Diamond\neg P\in\Gamma, on a aussi ¬P¬PΞ1\Diamond\Diamond\neg P\rightarrow\Diamond\neg P\in\Xi_1 et puisque Ξ1\Xi_1 est clos par substitution uniforme, ¬¬ϕ¬¬ϕΞ1\Diamond\Diamond\neg \neg\phi\rightarrow\Diamond\neg \neg\phi\in\Xi_1. Et donc chaque formule \Diamond\Diamond\rightarrow\Diamond appartient à Ξ1\Xi_1.
    Par définition de Ξ1Ξ2\Xi_1\longrightarrow \Xi_2 et Ξ2Ξ3\Xi_2\longrightarrow \Xi_3, pour une formule ϕ\phi quelconque, si ϕΞ3\phi\in\Xi_3, alors ϕΞ2\Diamond\phi\in\Xi_2 et ϕΞ1\Diamond\Diamond\phi\in\Xi_1. Et comme Ξ1\Xi_1 est clos par modus ponens, si à la fois ϕΞ1\Diamond\Diamond\phi\in\Xi_1 et ϕϕΞ1\Diamond\Diamond\phi\rightarrow\Diamond\phi\in\Xi_1, alors ϕΞ1\Diamond\phi\in\Xi_1. Cela prouve que pour toute formule ϕ\phi, si ϕΞ3\phi\in\Xi_3, alors ϕΞ1\Diamond\phi\in\Xi_1, et par conséquent Ξ1Ξ3\Xi_1\longrightarrow\Xi_3.
  3. MKDCn.b.d.\mathcal{M}_\text{\bf KD}\in\mathscr{C}_{n.b.d.} :
    il faut montrer que pour tout nœud Ξ1\Xi_1 de MKD\mathcal{M}_\text{\bf KD}, il existe Ξ2\Xi_2 tel que Ξ1Ξ2\Xi_1\longrightarrow \Xi_2.
    D'après le lemme (\longrightarrow et \Diamond), si ϕΞ1\Diamond\phi\in\Xi_1, alors il existe Ξ2\Xi_2 tel que Ξ1Ξ2\Xi_1\longrightarrow \Xi_2 et ϕΞ2\phi\in\Xi_2. Or l'axiome (D)\text{(D)} dit précisément PP\Box P\rightarrow\Diamond P. Comme Ξ1\Xi_1 est clos par substitution uniforme, la formule \Box\top\rightarrow\Diamond\top est dans Ξ1\Xi_1. Or Ξ1\Xi_1 vérifie nécessairement \Box\top (car une tautologie est vraie partout) et comme Ξ1\Xi_1 est clos par modus ponens, Ξ1\Diamond\top\in\Xi_1, et donc d'après le lemme (\longrightarrow et \Diamond), il existe Ξ2\Xi_2 tel que Ξ1Ξ2\Xi_1\longrightarrow \Xi_2 et Ξ2\top\in\Xi_2.
  4. MKD4Ctr.,n.b.d.\mathcal{M}_\text{\bf KD4}\in\mathscr{C}_{tr.,n.b.d.} :
    Conséquence de 2. et 3.
  5. MKTCref.\mathcal{M}_\text{\bf KT}\in\mathscr{C}_{ref.} :
    Il faut montrer que ΞΞ\Xi\longrightarrow \Xi est vérifié pour tout nœud Ξ\Xi de MKT\mathcal{M}_\text{\bf KT}.
    La formule (T)=PP\text{(T)}=\Box P\rightarrow P est équivalente à ¬¬PP\neg\Diamond\neg P\rightarrow P et par contraposition à ¬P¬P\neg P\rightarrow\diamond\neg P. Comme Ξ\Xi est clos par substitution uniforme, la formule ¬¬ϕ¬¬ϕ\neg \neg \phi\rightarrow\diamond\neg \neg\phi est dans Ξ\Xi et donc ϕϕ\phi\rightarrow\Diamond\phi est dans Ξ\Xi. La cloture par modus ponens permet alors de déduire que pour toute formule ϕΞ\phi\in\Xi, ϕΞ\Diamond\phi\in\Xi, ce qui est la condition nécessaire à la relation ΞΞ\Xi\longrightarrow \Xi.
  6. MS4Cref.,tr.\mathcal{M}_\text{\bf S4}\in\mathscr{C}_{ref.,tr.} :
    Conséquence de 2. et 5.
  7. MKBCsym.\mathcal{M}_\text{\bf KB}\in\mathscr{C}_{sym.} :
    il faut montrer que pour tout couple de nœuds Ξ1\Xi_1 et Ξ2\Xi_2 de MKB\mathcal{M}_\text{\bf KB}, Ξ1Ξ2\Xi_1\longrightarrow \Xi_2 alors Ξ2Ξ1\Xi_2\longrightarrow \Xi_1.
    (B)=PP\text{(B)}= P\rightarrow \Box\Diamond P . Comme Ξ1\Xi_1 est clos par substitution uniforme, les formules ϕϕ\phi\rightarrow\Box\Diamond\phi sont dans Ξ1\Xi_1. La cloture par modus ponens de Ξ1\Xi_1 nous dit alors que si ϕΞ1\phi\in\Xi_1, alors ϕΞ1\Box\Diamond\phi\in\Xi_1. Or d'après le lemme (\longrightarrow et \Box), si Ξ1Ξ2\Xi_1\longrightarrow\Xi_2 alors pour toute formule ϕ\phi, si ϕΞ1\Box\phi\in\Xi_1, alors ϕΞ2\phi\in\Xi_2. Par conséquent, pour tout ϕΞ1\phi\in\Xi_1, ϕΞ2\Diamond\phi\in\Xi_2, ce qui est la condition nécessaire pour définir Ξ2Ξ1\Xi_2\longrightarrow\Xi_1.
  8. MKB4Csym.tr.\mathcal{M}_\text{\bf KB4}\in\mathscr{C}_{sym.tr.} :
    Conséquence de 2. et 7.
  9. MKDBCsym.,n.b.d.\mathcal{M}_\text{\bf KDB}\in\mathscr{C}_{sym.,n.b.d.} :
    Conséquence de 3. et 7.
  10. MKTBCref.sym.\mathcal{M}_\text{\bf KTB}\in\mathscr{C}_{ref.sym.} :
    Conséquence de 5. et 7.
  11. MS5Cref.,sym.tr.\mathcal{M}_\text{\bf S5}\in\mathscr{C}_{ref.,sym.tr.} :
    Conséquence de 2. et 5. et 7.

On représente graphiquement par une flèche “CxX\mathscr{C}_x\longrightarrow\text{\bf X}” la relation de forte-complétude : “si ΓCxϕ\Gamma\models_{\mathscr{C}_x}\phi, alors ΓXϕ\Gamma\vdash_\text{\bf X}\phi”.

note

La notion de conséquence sémantique \models demande une satisfaction sur tous les modèle alors que la notion de conséquence syntaxique \vdash demande seulement l’existence d’une preuve.
Dit autrement, \models est définie avec un quantificateur universel \forall et \vdash avec un quantificateur existentiel \exists or la négation du quantificateur universel est le quantificateur existentiel et inversement.
Démontrer qu’une formule est non démontrable est donc très difficile du côté de la théorie de la démonstration puisque cela oblige à montrer que toutes les preuves échouent. Par contre, sur le versant sémantique, il suffit de trouver un modèle où la négation de la formule est satisfaite (un contre-exemple suffit).
C’est la correction qui nous permet le changement de versant (on passe de la syntaxe à la sémantique).
On peut trouver d’ailleurs un peu douloureux que la correspondance de loin la plus difficile à démontrer (la complétude) apporte si peu d’applications concrètes.


Suite : Différentes logiques modales