Logique modale

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

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

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

• $\varphi_n=\phi$


• chaque $\varphi_l$ vérifie l'une des quatre conditions suivantes :
  • $\varphi_l \in \text{\bf S}$ ($\varphi_l$ est un axiome)
  • $\varphi_l$ est obtenue par application de la règle du modus ponens à deux formules d'indice inférieurs $\varphi_j$ et $\varphi_k$ où $j , k < l$ ($\varphi_j = \varphi_k\rightarrow\varphi_l$)
  • $\varphi_l = \varphi_k[\theta /P]$ où $k < l$ (substitution d'une variable $P$ quelconque par une formule $\theta$ quelconque dans une formule d'indice inférieure)
  • $\varphi_l = [i]\varphi_j$ où $j < 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 $i\in I$ quelconque)

Exemple 1 :

Si $\text{\bf S}$ désigne l’ensemble des tautologies du calcul des propositions, alors la suite $\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 $\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 :

• $\varphi_1=P\rightarrow(P\lor\neg P)$ est une tautologie du calcul des propositions et donc un axiome du sydtème formel $\text{\bf S}$,
• $\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 $\Diamond Q$ à $P$ dans $\varphi_0$,
• $\varphi_3 = \Box (\Diamond Q\rightarrow(\Diamond Q\rightarrow\lor\neg\Diamond Q))$ est obtenu par nécessitation de $\varphi_1$,
• $\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 :

Exemple 2 :

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

Soient $\text{\bf S}$ un système formel et $\Gamma$ un ensemble de formules appelées hypothèses.
On écrit $\Gamma\vdash_\text{\bf S} \phi$ s’il existe un ensemble fini de formules $\set{\psi_1,\psi_2,\ldots,\psi_n}\subseteq\Gamma$ tel que la formule $(\psi_1\land\psi_2\land\ldots\land\psi_n)\rightarrow\phi$ puisse être prouvée dans le système formel $\text{\bf S}$. Autrement dit le séquent $\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$.

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

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

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

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

Pour montrer que $P\rightarrow\Box P$ n’est pas prouvable dans $\text{\bf K}$, il suffit donc de présenter un modèle (et le système $\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 :

Une logique modale normale $\mathbb{L}$ est un ensemble de formules qui contient le système formel $\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} $$

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

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

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

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

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

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

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.

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

Comme $\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 $\text{(4)}=\Box P\rightarrow\Box\Box P$ pour montrer que $\text{\bf K4}\not\subseteq \text{\bf KB}$.

$\text{(T)}$ et $\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 $\text{(4)}=\Box P\rightarrow\Box\Box P$ ni $\text{(5)}=\Diamond P\rightarrow\Box\Diamond P$.

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

$\text{\bf S}≤\text{\bf S'}$ si et seulement si $\vdash_\text{\bf S}\phi\rightarrow \,\vdash_\text{\bf S'}\phi$

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

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

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

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

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

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

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

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

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

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

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

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

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

Il faut montrer à la fois que :

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

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

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

• $\text{(T)}$ est valide dans tout système de transition réflexif.
• $\text{(B)}$ est valide dans tout système de transition symétrique.
• $\text{(4)}$ est valide dans tout système de transition transitif.
• $\text{(D)}$ est valide dans tout système de transition non borné à droite.
• $\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.

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

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

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

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

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

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

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

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

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

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

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

• $\Gamma_0=\Gamma$
• $\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}$
• $\displaystyle \Gamma_{max}=\bigcup_{n\in\mathbb{N}}\Gamma_n$

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

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

Soit $\mathbb{L}$ une logique modale normale et $\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle$ le modèle canonique associé à $\mathbb{L}$. Pour tout nœud $\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 $\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 $\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 $\mathbb{L}$-consistance de $\Gamma'$.

Soit $\mathbb{L}$ une logique modale normale et $\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle$ le modèle canonique associé à $\mathbb{L}$. Pour tout nœud $\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 $\psi_1,\ldots,\psi_k\in\Theta$ tels que $\vdash_\mathbb{L}(\psi_1\land\ldots\land\psi_k)\rightarrow\neg\phi$. Par nécessitation, $\vdash_\mathbb{L}\Box((\psi_1\land\ldots\land\psi_k)\rightarrow\neg\phi)$. Et par distributivité (utilisation de l’axiome $\text{(K)}$) $\vdash_\mathbb{L}\Box(\psi_1\land\ldots\land\psi_k)\rightarrow\Box\neg\phi$. Et puisque dans toute logique normale $\vdash_\mathbb{L}(\Box\psi_1\land\ldots\land\Box\psi_k)\rightarrow\Box(\psi_1\land\ldots\land\psi_k)$, on obtient finalement $\vdash_\mathbb{L}(\Box\psi_1\land\ldots\land\Box\psi_k)\rightarrow\Box\neg\phi$. Par conséquent $\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 $\mathbb{L}$-consistant, il suffit de prendre pour $\Gamma’$ l’ensemble $\Theta_{max}$ maximal $\mathbb{L}$-consistant donné par le lemme de Lindenbaum tel que $\Theta\subseteq\Theta_{max}$. On a bien ainsi un nœud de $N_\mathbb{L}$ contenant $\phi$.

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

$\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(\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 $\mathcal{V}_\mathbb{L}$.
• si $ht(\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 $\phi=(\psi_1\lor\psi_2)$, alors $\Gamma\Vdash(\psi_1\lor\psi_2)$ ssi $\Gamma\Vdash\psi_1$ ou $\Gamma\Vdash\psi_2$.
    Par hypothèse d'induction, $\Gamma\Vdash\psi_1$ ssi $\psi_1\in\Gamma$ et $\Gamma\Vdash\psi_2$ ssi $\psi_2\in\Gamma$. Et par maximalité de $\Gamma$, $\psi_1\in\Gamma$ ou $\psi_2\in\Gamma$ ssi $(\psi_1\lor\psi_2)\in\Gamma$.
  • si $\phi=(\psi_1\land\psi_2)$, alors $\Gamma\Vdash(\psi_1\lor\psi_2)$ ssi $\Gamma\Vdash\psi_1$ et $\Gamma\Vdash\psi_2$.
    Par hypothèse d'induction, $\Gamma\Vdash\psi_1$ ssi $\psi_1\in\Gamma$ et $\Gamma\Vdash\psi_2$ ssi $\psi_2\in\Gamma$. Or par $\mathbb{L}$-consistance, $\psi_1\in\Gamma$ et $\psi_2\in\Gamma$ ssi $(\psi_1\land\psi_2)\in\Gamma$.
  • si $\phi=(\psi_1\rightarrow\psi_2)$. On déduit ce cas de $\neg\psi_1\lor\psi_2$.
  • si $\phi=(\psi_1\leftrightarrow\psi_2)$. On déduit ce cas de $(\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 $\mathbb{L}$-consistance).

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

Pour chaque logique normale, nous allons choisir le modèle canonique $\mathcal{M}_\mathbb{L}=\langle N_\mathbb{L},A_\mathbb{L},\mathcal{V}_\mathbb{L}\rangle$ associé. Et pour le nœud $a$, nous allons prendre $\Gamma_{max}$. Le lemme de vérité nous dit alors que $\langle\mathcal{M}_\mathbb{L},\Gamma_{max}\rangle\Vdash\phi$ ssi $\phi\in\Gamma_{max}$. En conséquence, puisque $\Gamma\subseteq\Gamma_{max}$, il ressort que $\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 $\mathscr{C}$ considérée.

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