Théories et démonstrations

Jusqu'à présent, nous avons un langage permettant de construire des formules modales et nous avons une structure géométrique (le référentiel) permettant la caractérisation de certaines d'entre elles. Nous savons par exemple construire des modèles validant $p\; \to p,\; p\; \to p,\; (p\; \to p)\; \wedge (p\; \to p)$, ainsi que des contre-exemples justifiant l'indépendance sémantique de formules. Par exemple encore, on peut trouver une valuation sur un référentiel transitif et non réflexif validant $p\; \to p$ et possédant un monde où $p\; \to p$ est fausse. Je définis à présent une classe de théorie modale, et une notion de démonstration qui se comporte convenablement (de façon correcte et complète) relativement à la sémantique de Kripke. Grâce au résultat de complétude et de correction (soundness) les indépendances sémantiques (faciles à visualiser) démontrent automatiquement les indépendances syntactiques. Plus loin j'exhibe une sémantique plus générale attribuée à Scott et Montague [Chellas, 1980]. Définition Une théorie (formelle) est présentée par la donnée d'un ensemble de formules accompagnée de règles dite règles d'inférence, permettant la déduction de nouvelles formules. Une théorie est un ensemble de formules fermé pour l'application des règles d'inférence. Définition La présentation d'une théorie est l'ensemble des axiomes choisis et des règles d'inférence. Une théorie peut avoir de nombreuses présentations. Comme la logique modale est une extension de la logique propositionnelle classique, je présente d'abord une formalisation de celle-ci. Je choisis celle de [Kleene, 1952]. L'avantage de la formalisation de Kleene est que deux parmi ses ``affaiblissements" possibles donnent une formalisation pour la logique quantique et la logique intuitioniste respectivement. $A$, $B$, $C$ sont des métavariables représentant des formules quelconques. Il s'agit donc de schémas d'axiomes. J'utilise des schémas d'axiomes pour ne pas avoir de règles de substitution difficiles et longues à énoncer:

$$ AXIOMES\; \hspace{0.17em}:$A$ \to $(B$ \to $A)$ principe\; de\; l\text{'}a\; posteriori$(A$ \to $B)$ \to $((A$ \to $(B$ \to $C))$ \to $(A$ \to $C))$ $A$ \to $(B$ \to $A$ \wedge $B)$ $(A$ \to $C)$ \to $((B$ \to $C)$ \to $(A$ \vee $B$ \to $C))$ $A$ \to $(A$ \vee $B)$ $B$ \to $A$ \vee $B$ $(A$ \wedge $B)$ \to $A$ $(A$ \wedge $B)$ \to $B$ $(A$ \to $B)$ \to $((A$ \to $B)$ \to $A)$ $A$ \vee $A$ principe\; du\; tiers-exclu$$ $$ RÈGLES\; \hspace{0.17em}:$$ \{\; A\; ,\; \hspace{0.17em}\; A$ \to $BB\; \}$$ Modus\; Ponens$$

Logiques propositionnelles faibles On aura l'occasion de s'intéresser à quelques logiques plus faibles, du point de vue déductif (et donc plus puissantes du point de vue sémantique), que la logique classique. Il s'agit essentiellement de la logique intuitioniste et de la logique quantique. La logique intuitioniste (formalisée par Heyting, voir Troelstra Van Dalen 1988) peut être obtenue en remplaçant le principe du tiers-exclu par un principe plus faible: $p\; \to (p\; \to q)$. La logique quantique peut de même être obtenue en affaiblissant le principe de l'a posteriori (voir annexe C). Gödel (1933) et Goldblatt (1974) ont respectivement montré comment traduire la logique intuitioniste avec S4 (KT4), et la logique quantique avec B (KTB). Les logiques modales ``Kripke-convenables" Les logiques modales qui ont une sémantique de Kripke, possèdent comme axiomes et règles, outre les axiomes propositionnels de Kleene et la règle du modus ponens MP, l'axiome K et la règle de nécessitation $\{pp\}$. Un théorème est soit un axiome, soit une formule obtenue par un nombre fini d'applications de la règle du modus ponens, ou de la règle de nécessitation, à partir d'axiomes ou de théorèmes déjà démontrés. Cela va résulter des propositions qui vont suivre et du fait (qu'on a déjà vu) que K est respecté par tous les référentiels. Les principaux systèmes considérés sont K, KT, KT4 (appelé S4), KB, KD, KC, etc. où XYZ représente ici des logiques modales avec X, Y, Z comme axiomes, et sont fermées pour la modus ponens et la nécessitation. Notons que la ``fermeture pour le $$", la nécessitation, est une caractéristique de la sémantique de Kripke. On rencontrera des situations où la nécessitation, n'est pas vérifiée, et où, donc, d'autres sémantiques, comme celle plus générale des modèles minimaux (de Scott et Montague selon Chellas 1980) doivent être utilisées. On rencontrera des systèmes qui n'ont ni sémantique de Kripke, ni Scott-Montague (G$*$ par exemple).

Preuve. Le modus ponens est vérifié dans chaque monde. En effet, chaque monde vérifie la logique classique. Donc si $A$ est vraie dans tous les mondes, et si $A\; \to B$ est vraie dans tous les mondes, alors $B$ est vraie dans tous les mondes. Les référentiels respectent les formules obtenues par nécessitation sur des formules déjà respectées. En effet si $A$ est vraie dans tous les mondes d'un référentiel $W$, alors en particulier, pour chaque monde $\xi$, $A$ est vraie dans tous les mondes accessibles à partir de $\xi$, donc $A$ est vraie dans tous les mondes $\xi$ du référentiel, et donc $A$ est respectée aussi. En particulier si une proposition $A$ est respectée par une classe de référentiel, $A$ est respectée par cette classe de référentiel. Donc, le respect dans un référentiel est fermé pour la nécessitation et le modus ponens, et cela entraîne que tous les théorèmes de K (KT, K4, etc.) sont respectés dans un référentiel quelconque (réflexif. transitif, etc.) L'inverse est aussi vrai.

Idée de la preuve. La technique classique consiste à construire un modèle canonique qui satisfait tous les théorèmes de K (KT, K4, etc.), et seulement les théorèmes de K (KT, K4, etc.), et à montrer que ce modèle appartient à la classe de référentiels appropriée, c'est-à-dire quelconque (réflexif, transitif, etc.). Dans ce cas, si une formule est respectée dans tous les référentiels de la classe appropriée, elle est d'office satisfaite dans le modèle canonique et est donc un théorème de la théorie correspondante. Les logiciens depuis longtemps travaillent avec des modèles dont les mondes ou les univers sont des ensembles de formules, comme les modèles de Herbrand où les structures libres des algébristes. Un monde est défini par un ensemble consistant maximal de formules. Consistant est défini de façon purement syntaxique. Pour K (KT, K4, etc.), un ensemble de formules est consistant s'il n'existe pas de formule $F$₁, ..., F_n tel que K (KT, K4, etc.) démontre $(F$₁ ∧... ∧F_n). Si $E$ est un ensemble consistant de formules, on peut montrer que:

1. $E\; \{F\}$ est consistant ou $E\; \{F\}$ est consistant,
2. $E$ est contenu dans un ensemble consistant maximal, c'est-à-dire un ensemble consistant qui contient toute formule $F$ ou sa négation $F$.

Pour définir le modèle canonique, on doit définir d'une part le référentiel, c'est-à-dire l'ensemble $W$ des mondes et la relation $R$ d'accessibilité, et d'autre part la valuation $V$. On prend pour $W$, l'ensemble des mondes du modèle canonique, l'ensemble des ensembles maximaux consistants. La relation d'accessibilité R du modèle canonique est définie par

$aRbssi\{F\; F\; \in \alpha \}\; \subseteq \beta$

On peut alors montrer, c'est le point délicat, qu'on a bien pour chaque monde $\alpha \in W$ que si $F$ appartient à tous les mondes $\beta$ accessibles à partir de $\alpha$, alors $F$ appartient au monde $\alpha$. Reste à définir la valuation $V$: une formule atomique $p$ est vraie dans un monde si elle appartient à ce monde. Il n'est plus difficile alors de prouver, par induction sur la complexité des formules $F$, que $F$ est vraie dans le monde $\alpha$ ssi $F$ appartient à $\alpha$. Il ne reste plus alors qu'a montrer que les modèles canoniques de KT, KT4, ainsi de suite sont réflexifs, transitifs etc. Cela ne pose aucune difficulté (voir par exemple Boolos 79). % ne pas oublier : pas de métathéorème de %d éduction! sauf dans les dérivations qui %n'utilisent pas la nécessitation. C'est %utilisé dans la preuve de B! cf F95 page 54-55 Remarque Avec la logique modale, le métathéorème de déduction n'est pas valide dans les dérivations qui utilise la nécessitation. On ne peut pas, comme on le fait usuellement, décharger $p$ dans $\{pp\}$, pour prétendre, ayant obtenu $\{p\; \to p\}$, avoir démontrer $p\; \to p$. On a $\{pp\}$ (nécessitation), mais $p\; \to p$ est déjà contredit par le monde $\alpha$ dans le modèle de la figure A.4.

 
Figure A.4: Contre-exemple au métathéorème de déduction

Tant qu'on utilise pas la nécessitation, la procédure de déduction habituelle est bénigne.