Syntaxe

Variables propositionnelles

On considère un ensemble infini dénombrable \(\mathcal{V}\) dont les éléments sont appelés des variables propositionnelles. On note usuellement ces éléments par des lettres majuscules \(A, B, X, Y\dots\).

Par rapport à ce qui a été fait en mathématiques, ces variables représentent une sorte d'abstraction des formules atomiques des mathématiques. On a pu voir des formules comme « \(x = y\) » ou « \(n\) est pair », ici on les représentera par des variables.

On va alors s'intéresser à la logique en elle-même indépendamment des mathématiques.

Formules en tant qu'arbre

Grâce aux arbres, on peut donner une définition très précise des formules du calcul propositionnel :

Définition

Une formule du calcul propositionnel est un arbre ayant des nœuds binaires, étiquetés par \(\wedge, \vee, \rightarrow\) ou \(\leftrightarrow\), des nœuds unaires étiquetés par \(\neg\) et dont les feuilles sont étiquetées par \(\mathcal{V}\).

Remarque

Les symboles \(\wedge, \vee, \rightarrow\) et \(\leftrightarrow\) et \(\neg\) sont appelés des connecteurs logiques. Les quatre premiers sont dits binaires, ou d'arité 2, le dernier est dit unaire, ou d'arité 1.

Pour le moment, il ne s'agit que de symboles mais ils ne sont pas choisis au hasard et on leur attribuera un sens dans la suite de manière cohérente avec l'usage mathématique.

• \(\wedge\) est appelé la conjonction et se lit et
• \(\vee\) est appelé la disjonction et se lit ou
• \(\rightarrow\) est appelé l'implication et se lit implique
• \(\leftrightarrow\) est appelé l'équivalence et se lit équivaut
• \(\neg\) est appelé la négation et se lit non

Exemple

Les formules \(X\) et \(A \wedge (B \rightarrow \neg A)\) sont représentées par les arbres :

Arbres des formules \(X\) et \(A \wedge (B \rightarrow \neg A)\) : connecteurs en nœuds, variables en feuilles.

où \(A,B,X \in \mathcal{V}\).

De cette définition, on déduit directement la notion de taille et de hauteur d'une formule, il s'agit de la taille ou de la hauteur en tant qu'arbre.

On note \(\mathop{Var}(f)\) l'ensemble des variables apparaissant dans \(f\), c'est-à-dire l'ensemble des étiquettes des feuilles de l'arbre \(f\).

Définition inductive des formules

Il est plus traditionnel, bien qu'équivalent, de définir les formules sous la forme d'un ensemble inductif :

Définition

Les formules du calcul propositionnel sont les éléments du plus petit ensemble \(\mathcal{F}\) tel que :

• \(\mathcal{V} \subset \mathcal{F}\)
• \(\forall f, f' \in \mathcal{F}, \forall \square \in \{ \wedge, \vee, \rightarrow, \leftrightarrow \}\), \((f \square f') \in \mathcal{F}\).
• \(\forall f \in \mathcal{F}\), \(\neg f \in \mathcal{F}\).

On peut résumer cela sous la forme de l'équation inductive suivante :

\[ \mathcal{F} = \mathcal{V} \mid ( \mathcal{F} \wedge \mathcal{F} ) \mid ( \mathcal{F} \vee \mathcal{F} ) \mid ( \mathcal{F} \rightarrow \mathcal{F} ) \mid ( \mathcal{F} \leftrightarrow \mathcal{F} ) \mid \neg \mathcal{F} \]

Quand on définit ainsi l'ensemble, on peut se demander la nature réelle des objets que l'on a défini. Ici, il y a deux approches classiques :

• Les formules sont des mots sur l'alphabet \(\mathcal{V} \cup \{ (, ), \neg, \vee, \wedge, \rightarrow, \leftrightarrow \}\). Par exemple \(((X\vee Y)\wedge \neg Z)\in \mathcal{F}\) mais \((X\neg Y) \not \in \mathcal{F}\). C'est la vision historique des formules comme des chaînes de caractères.
• Les formules sont des arbres comme on l'a vu précédemment. L'avantage principal étant que tous ces arbres sont des formules sans ambigüité de lecture possible.

Que ce soit sous forme de chaîne ou d'arbre, on adopte une représentation plate des formules. Comme cela peut induire beaucoup de parenthèses, on va adopter une convention de priorité : en cas d'ambigüité, c'est la construction la plus prioritaire qui s'effectue.

On a les règles de priorité usuelles : \(\neg > \wedge, \vee > \rightarrow, \leftrightarrow\). On justifiera de plus dans la suite qu'on peut considérer \(\wedge\) et \(\vee\) comme étant associatives. Enfin, on convient que \(\rightarrow\) est associative à droite.

Exemple

• \((A \wedge (B \vee C))\) s'écrit \(A \wedge (B \vee C)\)
• \((A \vee (B \vee C))\) s'écrit \(A \vee B \vee C\)
• \((A \rightarrow (B \rightarrow C))\) s'écrit \(A \rightarrow B \rightarrow C\)
• \(((A \rightarrow B) \rightarrow C)\) s'écrit \((A \rightarrow B) \rightarrow C\)

Sémantique du calcul propositionnel

On considère ici un ensemble à deux éléments \(\mathbb{B} = \{ V, F \}\) dont les éléments sont appelés des valeurs de vérité. On parle de la valeur vraie pour \(V\) et fausse pour \(F\). C'est une pure convention, il n'y a aucune véracité mathématique pour appuyer ces termes. Quelque part, c'est la même situation que pour les bases directes.

Valuation et valeur de vérité d'une formule

Définition

Une valuation est une fonction \(v : \mathcal{V} \rightarrow \mathbb{B}\).

C'est une forme d'environnement pour les formules comme pourrait l'être une affectation de valeurs à des variables pour évaluer des expressions arithmétiques. On va donc pouvoir s'appuyer sur une telle valuation pour définir la valeur de vérité d'une formule comme une évaluation :

Définition

Soit \(v\) une valuation et \(f \in \mathcal{F}\). On appelle valeur de vérité de \(f\) sous la valuation \(v\), l'élément \([f]_v \in \mathbb{B}\) défini inductivement par :

• \(\forall X \in \mathcal{V}, [X]_v = v(X)\)
• \(\forall f \in \mathcal{F}, [\neg f]_v = \begin{cases} V & \text{si } [f]_v = F \\ F & \text{sinon} \end{cases}\)
• \(\forall f, f' \in \mathcal{F}, \forall \square \in \{\wedge, \vee, \rightarrow, \leftrightarrow \}\) on détermine \([f \square f']_v\) en fonction de \([f]_v\) et \([f']_v\) selon la table suivante :

\([f]_v\)	\([f']_v\)	\([f \vee f']_v\)	\([f \wedge f']_v\)	\([f \rightarrow f']_v\)	\([f \leftrightarrow f']_v\)
V	V	V	V	V	V
V	F	V	F	F	F
F	V	V	F	V	F
F	F	F	F	V	V

Exemple

Si \(f = A \vee B \rightarrow A \wedge C\) et qu'on sait que \(v(A) = v(C) = V\) et \(v(B) = F\), alors \([A \vee B]_v = V\) et \([A \wedge C]_v = V\) selon la table. On a alors \([f]_v = V\).

Table de vérité

Une formule ne pouvant faire apparaître qu'un nombre fini de variables, les valuations comportent beaucoup d'informations n'ayant aucune influence sur la valeur de vérité de \(f\). Cela est précisé dans le théorème suivant :

Théorème

Soit \(f \in \mathcal{F}\) et \(v,v' : \mathcal{V} \rightarrow \mathbb{B}\) deux valuations.

Si \(\forall X \in \mathop{Var}(f), v(X) = v'(X)\) alors \([f]_v = [f]_{v'}\).

Preuve

Par induction structurelle sur \(f\), on montre la propriété \(P(f)\) : « pour toutes valuations \(v, v'\) coïncidant sur \(\mathop{Var}(f)\), \([f]_v = [f]_{v'}\) ».

• Si \(X \in \mathcal{V}\) et \(f = X\), alors \(X \in \mathop{Var}(f)\) et \([f]_v = v(X) = v'(X) = [f]_{v'}\).
• Si \(P(f)\) est vraie et si \(v, v'\) coïncident sur \(\mathop{Var}(\neg f) = \mathop{Var}(f)\), alors \([f]_v = [f]_{v'}\) et donc \([\neg f]_v = V \iff [f]_v = F \iff [f]_{v'} = F \iff [\neg f]_{v'} = V\). Ainsi, comme il n'y a que deux valeurs possibles, \([\neg f]_v = [\neg f]_{v'}\).
• Si \(P(f)\) et \(P(f')\) sont vraies et si \(v, v'\) coïncident sur \(\mathop{Var}(f \square f') = \mathop{Var}(f) \cup \mathop{Var}(f')\), elles coïncident sur \(\mathop{Var}(f)\) et sur \(\mathop{Var}(f')\), donc \([f]_v = [f]_{v'}\) et \([f']_v= [f']_{v'}\). Or, \([f \square f']_v\) ne dépend que de \([f]_v\) et \([f']_v\) selon les tables de la définition pour \(\square \in \{ \vee, \wedge, \rightarrow, \leftrightarrow \}\). On en conclut directement que \([f \square f']_v = [f \square f']_{v'}\).

Ainsi, on peut se concentrer sur les valeurs de vérité associées aux variables présentes dans une formule. Ce faisant, on introduit le concept de tables de vérité :

Définition

Soit \(f \in \mathcal{F}\) dont les \(n\) variables (deux à deux distinctes) sont \(X_1, \dots, X_n\).

On appelle table de vérité de \(f\) une fonction

\[ T_f : \mathbb{B}^n \rightarrow \mathbb{B} \]

telle que pour toute valuation \(v\) on ait

\[ [f]_v = T_f(v(X_1), \dots, v(X_n)) \]

Théorème

Toute formule a une table de vérité et elle est unique à l'ordre près de l'énumération de ses variables.

Preuve

Soit \(f \in \mathcal{F}\) et \(X_1, \dots, X_n\) ses variables.

1. Si \(b = (b_1, \dots, b_n)\in \mathbb{B}^n\), on note \(v_b\) la valuation définie par

   \[ v_b : Y \in \mathcal{V} \mapsto \begin{cases} b_i & \text{ si } Y = X_i \text{ pour } i \in \range{1}{n} \\ F & \text{ sinon } \end{cases} \]

   On pose alors \(T_f : b \mapsto [f]_{v_b}\).

2. Soit \(v'\) une valuation et \(b = (v'(X_1), \dots, v'(X_n))\). On a \(v_b\) et \(v'\) identiques sur les variables de \(f\), donc d'après le théorème précédent \([f]_{v'} = [f]_{v_b} = T_f(b)\). Ainsi \(T_f\) est une table de vérité de \(f\).

3. Si \(T'\) est une autre table de vérité pour le même ordre d'énumération, on a pour \(b \in \mathbb{B}^n\), par définition de la table appliquée à la valuation \(v_b\), \(T'(b) = [f]_{v_b} = T_f(b)\). Donc \(T' = T_f\).

Remarque

On représente usuellement une table de vérité sous la forme d'une table avec une colonne par variable et une colonne pour la valeur de \(f\).

Par exemple, pour \(f = (A \wedge B) \vee C\) :

A	B	C	f
V	V	V	V
V	V	F	V
V	F	V	V
V	F	F	F
F	V	V	V
F	V	F	F
F	F	V	V
F	F	F	F

Satisfiabilité, tautologie

Définition

Soit \(f \in \mathcal{F}\) et \(v : \mathcal{V} \rightarrow \mathbb{B}\).

On note \(v \models f\) quand \([f]_v = V\) et on dit que \(v\) est un modèle de \(f\). On note ainsi \(\mathop{Mod}(f) = \enscomp{v}{v \models f}\).

• Si \(\mathop{Mod}(f) \neq \emptyset\) on dit que \(f\) est satisfiable.
• Si \(\mathop{Mod}(f) = \mathbb{B}^\mathcal{V}\) on dit que \(f\) est une tautologie.
• Si \(\mathop{Mod}(f) = \emptyset\) on dit que \(f\) est une antilogie.

Théorème

• \(f\) est une tautologie ssi \(T_f\) est constante de valeur \(V\)
• \(f\) est une antilogie ssi \(T_f\) est constante de valeur \(F\)
• \(f\) est satisfiable ssi \(V \in T_f(\mathbb{B}^n)\).

Preuve

Pour toute valuation \(v\), \([f]_v = T_f(v(X_1), \dots, v(X_n))\) et, réciproquement, tout \(b \in \mathbb{B}^n\) s'écrit \((v_b(X_1), \dots, v_b(X_n))\) avec la valuation \(v_b\) de la preuve précédente. Ainsi \(\enscomp{[f]_v}{v \in \mathbb{B}^\mathcal{V}} = T_f(\mathbb{B}^n)\), d'où les trois équivalences.

Exemple

• \(X \vee \neg X\) est une tautologie appelée le tiers-exclu.
• \(X \wedge \neg X\) est une antilogie : c'est la contradiction, dont la négation \(\neg(X \wedge \neg X)\) est le principe de non-contradiction.
• \(((A \rightarrow B) \rightarrow A) \rightarrow A\) est une tautologie.

Remarque

Il est pratique d'introduire des formules constantes \(\top\) et \(\perp\) pour représenter une tautologie et une antilogie quelconque.

Équivalence entre deux formules

Définition

Soient \(f, f'\in \mathcal{F}\). On dit que \(f\) et \(f'\) sont équivalentes, et l'on note \(f \iff f'\) ou \(f \equiv f'\), lorsque \(f\) et \(f'\) ont mêmes modèles, c'est-à-dire lorsque \(\mathop{Mod}(f) = \mathop{Mod}(f')\).

Théorème

L'équivalence logique est une relation d'équivalence.

Remarque

• Cela signifie que deux formules équivalentes ne peuvent être distinguées par leur valeur de vérité sous une valuation.
• \(f\) est une tautologie si et seulement si \(f \iff \top\)
• \(f\) est une antilogie si et seulement si \(f \iff \perp\)

Théorème

Soient \(f, f' \in \mathcal{F}\) avec \(\mathop{Var}(f) = \mathop{Var}(f')\), variables énumérées dans le même ordre pour les deux tables.

On a \(f \iff f'\) si et seulement si \(T_f = T_{f'}\).

Remarque

Cela permet de vérifier l'équivalence entre deux formules en établissant les deux tables de vérité et en vérifiant qu'elles sont identiques. Comme une telle table comporte \(2^n\) lignes pour \(n\) variables, c'est souvent fastidieux.

Il y a de nombreuses équivalences logiques qui sont fondamentales car elles permettent de simplifier les formules pour travailler sur des formules plus simples. On va démontrer ici les principales :

Théorème

Soient \(P, Q, R \in \mathcal{V}\)

• \(\neg \neg P \iff P\)
• \(P \rightarrow Q \iff \neg P \vee Q\)
• \(P \leftrightarrow Q \iff (P \wedge Q) \vee (\neg P \wedge \neg Q)\)

Lois de de Morgan :

• \(\neg (P \vee Q) \iff \neg P \wedge \neg Q\)
• \(\neg (P \wedge Q) \iff \neg P \vee \neg Q\)

Commutativité :

• \(P \wedge Q \iff Q \wedge P\)
• \(P \vee Q \iff Q \vee P\)

Associativité :

• \(P \wedge (Q \wedge R) \iff (P \wedge Q) \wedge R\)
• \(P \vee (Q \vee R) \iff (P \vee Q) \vee R\)

Distributivité :

• \(P \wedge (Q \vee R) \iff (P \wedge Q) \vee (P \wedge R)\)
• \(P \vee (Q \wedge R) \iff (P \vee Q) \wedge (P \vee R)\)

Preuve

Il suffit de faire de fastidieuses vérifications à l'aide de tables de vérité (le théorème précédent s'applique car les deux membres ont les mêmes variables). Par exemple, pour la première loi de distributivité, les deux membres valent \(V\) exactement lorsque \(P\) vaut \(V\) et l'un de \(Q\), \(R\) vaut \(V\). On peut se contenter de ne démontrer qu'une partie d'entre elles grâce à la double négation et aux lois de de Morgan.

Substitution et congruence

On vient de démontrer des équivalences mais le fait d'utiliser des variables semble en restreindre la portée. En effet, si on considère la formule \(\neg \neg (A \rightarrow B)\) il ne semble pas possible d'en déduire directement qu'elle est équivalente à \(A \rightarrow B\) car l'équivalence \(\neg \neg X \iff X\) ne s'applique que pour une variable.

Or, dès le départ, les variables propositionnelles ne se voulaient qu'être des abstractions sur des propriétés. On va démontrer ici un lemme de substitution qui permettra de déduire de nouvelles équivalences en remplaçant une variable par une formule.

Définition

Soit \(f, g \in \mathcal{F}\) et \(X \in \mathcal{V}\). On définit la substitution de \(X\) par \(g\), notée \(f[g/X]\) par induction ainsi :

• Si \(Y \in \mathcal{V} \backslash \{ X \}\), \(Y[g/X] = Y\)
• \(X[g/X] = g\)
• Si \(f \in \mathcal{F}\), \((\neg f)[g/X] = \neg f[g/X]\)
• Si \(\square \in \{\wedge, \vee, \rightarrow, \leftrightarrow\}\) et \(f, f' \in \mathcal{F}\), \((f \square f')[g/X] = f[g/X] \square f'[g/X]\)

Lemme

Soit \(f, g \in \mathcal{F}, X \in \mathcal{V}\) et \(v : \mathcal{V} \rightarrow \mathbb{B}\).

On pose \(v' : \mathcal{V} \rightarrow \mathbb{B}\) telle que \(v'(X) = [g]_v\) et \(v'(Y) = v(Y)\) pour \(Y \neq X\).

On a alors \(\left[ f[g/X] \right]_v = [f]_{v'}\).

Preuve

Par induction structurelle sur \(f\) (à \(g\), \(X\) et \(v\) fixés).

• Si \(f = X\), \(\left[ X[g/X] \right]_v = [g]_v = v'(X) = [X]_{v'}\).
• Si \(f = Y \in \mathcal{V} \setminus \{ X \}\), \(\left[ Y[g/X] \right]_v = [Y]_v = v(Y) = v'(Y) = [Y]_{v'}\).
• Si \(f = \neg f_1\) avec la propriété vraie pour \(f_1\), alors \(\left[ (\neg f_1)[g/X] \right]_v = \left[ \neg (f_1[g/X]) \right]_v\) est la négation de \(\left[ f_1[g/X] \right]_v = [f_1]_{v'}\), c'est donc \([\neg f_1]_{v'}\).
• Si \(f = f_1 \square f_2\) avec la propriété vraie pour \(f_1\) et \(f_2\), alors \(\left[ (f_1 \square f_2)[g/X] \right]_v = \left[ f_1[g/X] \square f_2[g/X] \right]_v\) se lit dans la table de \(\square\) à partir de \(\left[ f_1[g/X] \right]_v = [f_1]_{v'}\) et \(\left[ f_2[g/X] \right]_v = [f_2]_{v'}\) : c'est donc \([f_1 \square f_2]_{v'}\).

Théorème

Soient \(f,g,h \in \mathcal{F}\) et \(X \in \mathcal{V}\).

Si \(f \equiv g\), alors \(f[h/ X] \equiv g[h / X]\).

Preuve

Soit \(v\) une valuation, on définit \(v'\) comme dans le lemme précédent avec \(v'(X) = [h]_v\). On a alors \(\left[ f[h/X] \right]_v = [f]_{v'}\) et \(\left[ g[h/X] \right]_v = [g]_{v'}\). Or, par hypothèse, \([f]_{v'} = [g]_{v'}\).

On a ainsi l'égalité \(\left[ f[h/X] \right]_v = \left[ g[h/X] \right]_v\) et donc \(f[h/X] \equiv g[h/X]\).

Le fait de faire passer des équivalences sous des opérations, ici les connecteurs logiques, est traditionnellement appelé une congruence. On a ici le théorème suivant :

Théorème

Soient \(f, g, h \in \mathcal{F}\) où \(f \equiv g\).

On a :

• \(\neg f \equiv \neg g\)
• \(\forall \square \in \{\wedge, \vee, \rightarrow, \leftrightarrow \}\), \(f \square h \equiv g \square h\) et \(h \square f \equiv h \square g\).

Preuve

Soit \(v\) une valuation. Par hypothèse \([f]_v = [g]_v\). Or \([\neg f]_v\) ne dépend que de \([f]_v\), et \([f \square h]_v\) (resp. \([h \square f]_v\)) ne dépend que de \([f]_v\) et \([h]_v\) : on obtient donc les mêmes valeurs en remplaçant \(f\) par \(g\).

Conséquence logique

Définition

Soit \(f, g \in \mathcal{F}\), on dit que \(f\) est conséquence logique de \(g\) lorsque \(\mathop{Mod}(g) \subset \mathop{Mod}(f)\).

Autrement dit, lorsque pour toute valuation \(v\), \([g]_v = V\) implique \([f]_v = V\).

On note alors \(g \models f\).

Si \(\Gamma \subset \mathcal{F}\) on note \(\Gamma \models f\) s'il existe \(g_1, \dots, g_n \in \Gamma\) tels que \(g_1 \wedge \dots \wedge g_n \models f\) (avec la convention qu'une conjonction vide, pour \(n = 0\), vaut \(\top\)). On note aussi \(g_1, \dots, g_p \models f\) pour \(\{ g_1, \dots, g_p \} \models f\).

Lemme

Soient \(\Gamma,\Delta \subset \mathcal{F}\) et \(f \in \mathcal{F}\).

Si \(\Gamma \models f\) alors \(\Gamma \cup \Delta \models f\).

Preuve

Par définition, il existe \(g_1, \dots, g_n \in \Gamma\) tels que \(g_1 \wedge \dots \wedge g_n \models f\). Comme ces formules sont aussi dans \(\Gamma \cup \Delta\), on a directement \(\Gamma \cup \Delta \models f\).

On aura aussi besoin du fait suivant : si \(g \models f\), alors pour toute formule \(h\), \(g \wedge h \models f\). En effet, soit \(v\) une valuation telle que \(v \in \mathop{Mod}(g \wedge h)\). On a donc \([g \wedge h]_v = V\) et par définition de la valeur de vérité d'une conjonction, \([g]_v = [h]_v = V\). Or, comme \([g]_v = V\) et que \(g \models f\) on a \([f]_v = V\). On vient de montrer \(g \wedge h \models f\). Avec la commutativité et l'associativité de \(\wedge\), on en déduit que si une conjonction de formules de \(\Gamma\) a \(f\) pour conséquence, il en est de même de toute conjonction contenant ces formules.

Théorème

Soient \(f, g \in \mathcal{F}\). Les propriétés suivantes sont équivalentes :

1. \(g \models f\)
2. \(g, \neg f \models \perp\)
3. \(g \rightarrow f\) est une tautologie

Preuve

\(1. \Rightarrow 2.\) : Supposons que \(g \models f\) et supposons qu'il existe une valuation \(v\) telle que \([g \wedge \neg f]_v = V\). On a donc \([g]_v = [\neg f]_v = V\) par l'argument usuel sur la table de la conjonction. Ainsi \([f]_v = F\) mais comme \(g \models f\), on a \([f]_v = V\). Or, une formule a une unique valeur de vérité, donc on aboutit à une contradiction. Ainsi \(\mathop{Mod}(g \wedge \neg f) = \emptyset\) et \(g \wedge \neg f \models \perp\) vu que \(\mathop{Mod}(\perp) = \emptyset\).

\(2. \Rightarrow 3.\) Supposons que \(g, \neg f \models \perp\). Une conjonction de formules parmi \(g, \neg f\) a pour conséquence \(\perp\), donc d'après le fait établi dans la preuve du lemme précédent, \(g \wedge \neg f \models \perp\), c'est-à-dire \(\mathop{Mod}(g \wedge \neg f) \subset \mathop{Mod}(\perp) = \emptyset\). Soit \(v\) une valuation et supposons, par l'absurde, que \([g \rightarrow f]_v = F\). Alors, de par la table de \(\rightarrow\), cela signifie nécessairement que \([g]_v = V\) et \([f]_v = F\). Donc \([g \wedge \neg f]_v = V\). Contradiction car on a trouvé un modèle de \(g \wedge \neg f\).

\(3. \Rightarrow 1.\) Supposons que \(g \rightarrow f\) soit une tautologie et soit \(v\) une valuation telle que \([g]_v = V\). Comme \([g \rightarrow f]_v = V\) on a nécessairement \([f]_v = V\) par étude de la table de \(\rightarrow\). Donc, on a bien \(g \models f\).

Remarque

Le fait de se ramener à montrer \(\Gamma, \neg f \models \perp\) pour prouver que \(\Gamma \models f\) est un principe très important appelé la réfutation. Il est à la base de la méthode de résolution, introduite par le logicien John Alan Robinson, qui sert de base au langage de programmation logique Prolog.

Théorème

Si \(f \models g\) et \(g \models h\) alors \(f \models h\).

Preuve

Il s'agit juste de la transitivité de l'inclusion sur les modèles.

Remarque

Cette propriété, appelée syllogisme hypothétique, est, comme le Modus Ponens (si \(f\) et \(f \rightarrow g\) sont vraies alors \(g\) l'est), un principe fondamental du raisonnement identifié très tôt dans l'histoire des mathématiques.

Formes normales

On a vu beaucoup d'équivalences logiques dans la partie précédente, elles permettent de réécrire une formule sous une forme plus pratique pour raisonner. On parle alors de forme normale.

Comme on a pu le voir, les opérateurs \(\rightarrow\) et \(\leftrightarrow\) peuvent s'exprimer avec les trois autres. On va donc considérer ici uniquement des formules avec les opérateurs \(\vee, \wedge, \neg\).

Forme normale conjonctive et disjonctive

Définition

Une formule de la forme \(X\) ou \(\neg X\) avec \(X \in \mathcal{V}\) est appelée un littéral, on précise parfois positif ou négatif.

Une formule de la forme \(l_1 \vee \dots \vee l_n\) où les \(l_i\) sont des littéraux est appelée une clause. On parle de clause vide pour \(\perp\).

Une formule de la forme \(C_1 \wedge \dots \wedge C_m\) où les \(C_j\) sont des clauses est appelée une forme normale conjonctive (FNC). On parle de FNC vide pour \(\top\).

Exemple

• \(A \wedge (\neg A \vee B) \wedge \perp\) est une FNC.

En vertu de l'associativité des connecteurs, on note de manière synthétique

\[ \bigwedge_{i=1}^n \bigvee_{j=1}^{n_i} l_{i,j} \]

une FNC, où les \(l_{i,j}\) sont des littéraux.

Définition

On définit de même les formes normales disjonctives (FND) comme les disjonctions de conjonctions de littéraux.

Ce sont les formules sous la forme :

\[ \bigvee_{i=1}^n \bigwedge_{j=1}^{n_i} l_{i,j} \]

où les \(l_{i,j}\) sont des littéraux.

Mise sous forme normale disjonctive

Soit \(f \in \mathcal{F}\) dont les variables sont \(X_1, \dots, X_n\), on peut passer de sa table de vérité à une FND en posant :

\[ \Phi(f) = \bigvee_{(b_1, \dots, b_n) \in T_f^{-1}(\{V\}) } \bigwedge_{i=1}^n l(X_i,b_i) \]

où \(l(X_i,V) = X_i\) et \(l(X_i,F) = \neg X_i\) (si \(T_f^{-1}(\{V\})\) est vide, \(\Phi(f)\) est la disjonction vide, c'est-à-dire \(\perp\)).

On a \(\Phi(f) \equiv f\) car \(\Phi(f)\) a été construite pour avoir la même table de vérité que \(f\) : pour une valuation \(v\), la conjonction \(\bigwedge_{i=1}^n l(X_i,b_i)\) est vraie si et seulement si \(v(X_i) = b_i\) pour tout \(i\), donc \([\Phi(f)]_v = V\) si et seulement si \((v(X_1), \dots, v(X_n)) \in T_f^{-1}(\{V\})\), c'est-à-dire si et seulement si \([f]_v = V\).

On remarque tout de suite que la taille de \(\Phi(f)\) dépend du nombre de valeurs à \(V\) dans sa table de vérité. Pour une tautologie portant sur \(n\) variables, \(\Phi(f)\) est ainsi une disjonction de \(2^n\) conjonctions de \(n\) littéraux, de taille \(\Theta(n 2^n)\).

Mise sous forme normale conjonctive

Définition

Soit \(f \in \mathcal{F}\), on définit la formule \(\varphi(f)\) ainsi par induction structurelle :

• Si \(X \in \mathcal{V}\), \(\varphi(X) = X\)
• Si \(f \in \mathcal{F}\),
  • Soit \(f = X \in \mathcal{V}\) et \(\varphi(\neg X) = \neg X\)
  • Soit \(f = \neg f'\) et \(\varphi(\neg f) = \varphi(f')\)
  • Soit \(f = g \wedge h\) et \(\varphi(\neg f) = \varphi(\neg g) \vee \varphi(\neg h)\).
  • Soit \(f = g \vee h\) et \(\varphi(\neg f) = \varphi(\neg g) \wedge \varphi(\neg h)\).
• Si \(f, f' \in \mathcal{F}\), \(\varphi(f \vee f') = \varphi(f) \vee \varphi(f')\) et \(\varphi(f \wedge f') = \varphi(f) \wedge \varphi(f')\).

Théorème

On a \(\varphi(f) \iff f\) et dans \(\varphi(f)\) les négations appartiennent toutes à des littéraux.

Preuve

On remarque d'abord que \(\varphi\) est bien définie : chaque appel récursif porte sur une formule de taille strictement inférieure (\(\neg f'\) est plus petite que \(\neg \neg f'\), \(\neg g\) et \(\neg h\) sont plus petites que \(\neg (g \wedge h)\), etc.).

On montre alors par récurrence forte sur la taille de \(f\) que \(\varphi(f) \equiv f\) et que les négations de \(\varphi(f)\) portent toutes sur des variables. Les cas \(f = X\), \(f = \neg X\), \(f = g \vee h\) et \(f = g \wedge h\) découlent directement de l'hypothèse de récurrence (et de la congruence pour l'équivalence). Pour \(f = \neg \neg f'\), on utilise \(\neg \neg f' \equiv f'\) ; pour \(f = \neg(g \wedge h)\) (resp. \(\neg (g \vee h)\)), on utilise la loi de de Morgan \(\neg(g \wedge h) \equiv \neg g \vee \neg h\) (resp. \(\neg (g \vee h) \equiv \neg g \wedge \neg h\)), ces équivalences entre formules étant obtenues à partir de celles entre variables par le théorème de substitution, puis l'hypothèse de récurrence appliquée à \(\neg g\) et \(\neg h\).

Il est possible de passer de FND à FNC à l'aide d'une négation et des lois de de Morgan. On en déduit donc une manière d'obtenir une FNC équivalente à \(f\) : on met \(\neg \Phi(\neg f) \equiv f\) sous FNC en éliminant la négation.

Cependant, on peut obtenir une FNC plus directement par induction comme on peut le voir dans la définition suivante.

Définition

Soit \(f\) une formule dont les négations appartiennent toutes à des littéraux, on définit \(\psi(f)\) par induction structurelle :

• \(\psi(l) = l\) si \(l\) est un littéral
• \(\psi(f \wedge g) = \psi(f) \wedge \psi(g)\)
• Si \(\psi(f) = f_1 \wedge f_2\) alors \(\psi(f \vee g) = \psi(f_1 \vee g) \wedge \psi(f_2 \vee g)\).
• Si \(\psi(f)\) n'est pas une conjonction et \(\psi(g) = g_1 \wedge g_2\) alors \(\psi(f \vee g) = \psi(f \vee g_1) \wedge \psi(f \vee g_2)\).
• Si ni \(\psi(f)\) ni \(\psi(g)\) ne sont des conjonctions alors \(\psi(f \vee g) = \psi(f) \vee \psi(g)\).

Théorème

Soit \(f \in \mathcal{F}\), \(\psi(\varphi(f)) \equiv f\) et \(\psi(\varphi(f))\) est en forme normale conjonctive.

Preuve

Esquisse. Pour deux FNC \(a\) et \(b\), on définit \(D(a, b)\) par : \(D(a_1 \wedge a_2, b) = D(a_1, b) \wedge D(a_2, b)\), sinon \(D(a, b_1 \wedge b_2) = D(a, b_1) \wedge D(a, b_2)\), et sinon (deux clauses) \(D(a, b) = a \vee b\). Par récurrence sur la taille de \(a\) plus celle de \(b\), \(D(a, b)\) est bien définie, est une FNC et \(D(a,b) \equiv a \vee b\) par distributivité (et congruence).

On vérifie ensuite que \(\psi(c) = c\) pour toute FNC \(c\), puis, par récurrence sur la somme des tailles de \(\psi(f)\) et \(\psi(g)\), que \(\psi(f \vee g) = D(\psi(f), \psi(g))\) : par exemple si \(\psi(f) = f_1 \wedge f_2\), alors \(\psi(f_1) = f_1\) est plus petite que \(\psi(f)\) et \(\psi(f \vee g) = \psi(f_1 \vee g) \wedge \psi(f_2 \vee g) = D(f_1, \psi(g)) \wedge D(f_2, \psi(g)) = D(\psi(f), \psi(g))\). Ceci assure que \(\psi\) est bien définie, et une induction structurelle sur \(f\) montre alors que \(\psi(f)\) est une FNC équivalente à \(f\). On conclut avec le théorème précédent appliqué à \(\varphi(f)\).

Remarque

Il est possible d'obtenir ainsi une formule de taille exponentielle.

L'exemple caractéristique est

\[ \bigvee_{i=1}^n (X_{i,1} \wedge X_{i,2}) \equiv \bigwedge_{a_1 \in \{1,2\}, \dots, a_n \in \{1,2\}} \left( X_{1,a_1} \vee \dots \vee X_{n,a_n} \right) \]

où la FNC de droite comporte \(2^n\) clauses.

On passe ainsi d'une formule de taille \(O(n)\) à une formule de taille \(O(2^n)\).

Il est possible d'implémenter directement cette méthode :

type formula = Var of string
    | And of formula * formula
    | Or of formula * formula
    | Not of formula

let rec elim_not f = match f with
    | Var s -> Var s
    | Not (Var s) -> Not (Var s)
    | Not (Not f) -> elim_not f
    | Not (Or (f1,f2)) -> And( elim_not(Not f1), elim_not(Not f2) )
    | Not (And (f1,f2)) -> Or( elim_not(Not f1), elim_not(Not f2) )
    | Or(f1, f2) -> Or(elim_not f1, elim_not f2)
    | And(f1, f2) -> And(elim_not f1, elim_not f2)

let rec distrib_or f = match f with
    | Var _ -> f
    | Not (Var _) -> f
    | And(f1,f2) -> And(distrib_or f1, distrib_or f2)
    | Or(f1,f2) -> begin
            match distrib_or f1 with
            | And(f11, f12) -> And(distrib_or (Or(f11,f2)), 
                                   distrib_or (Or(f12,f2)))
            | f1' -> match distrib_or f2 with
                | And (f21, f22) -> And(distrib_or(Or(f1', f21)), 
                                        distrib_or(Or(f1',f22)))
                | f2' -> Or(f1', f2')
            end
    | _ -> failwith "Formule avec négation en dehors des littéraux"

let fnc f = distrib_or (elim_not f)

Problème SAT

Définition

Un des problèmes les plus importants en logique et plus largement en informatique est le problème SAT :

Problème SAT

• Entrée : une formule \(f\), le plus souvent en FNC.
• Sortie : un booléen indiquant si \(f\) est satisfiable.

\(k\)-SAT

Le problème suivant permet un plus grand contrôle sur les formules.

Problème \(k\)-SAT

• Entrée : une formule \(f\) en FNC dont les clauses comportent au plus \(k\) littéraux.
• Sortie : un booléen indiquant si \(f\) est satisfiable.

Naturellement, si on sait résoudre \(k\)-SAT pour tout \(k\), alors on sait résoudre SAT vu que les formules sont finies.

1-SAT

Les formules à résoudre sont des conjonctions de littéraux vu que les clauses sont réduites à un littéral. Or, soit cette conjonction contient deux littéraux opposés auquel cas \(f \equiv \perp\), ou alors elle est satisfiable en considérant \(v(X) = V\) si \(X\) apparaît positivement et \(v(X) = F\) sinon.

2-SAT

Pour résoudre 2-SAT on va construire un graphe en transformant les clauses en implications :

\[ X \vee Y \iff \neg X \rightarrow Y \iff \neg Y \rightarrow X \]

\[ \neg X \vee Y \iff X \rightarrow Y \iff \neg Y \rightarrow \neg X \]

\[ \neg X \vee \neg Y \iff X \rightarrow \neg Y \iff Y \rightarrow \neg X \]

On peut alors construire un graphe où les sommets sont les littéraux apparaissant dans une formule ainsi que leur négation, et où l'on met un arc de \(l\) vers \(l'\) quand une clause est équivalente à \(l \rightarrow l'\) (chaque clause donne ainsi deux arcs).

Un chemin dans ce graphe est une chaîne d'implications. On peut montrer que \(f\) est satisfiable si et seulement s'il n'existe aucune variable \(X\) telle qu'il y ait à la fois un chemin de \(X\) à \(\neg X\) et un chemin de \(\neg X\) à \(X\) (un chemin de \(X\) à \(\neg X\) seul impose simplement \(v(X) = F\)). Or, pour déterminer cela, il suffit de calculer la fermeture transitive du graphe, par exemple avec des parcours successifs, ou avec Floyd-Warshall. Cela se fait donc en temps et en espace polynomial dans le nombre de variables. On peut même le faire en temps linéaire en calculant les composantes fortement connexes du graphe.

3-SAT

On peut montrer un théorème assurant que ce chapitre aura un nombre fini de paragraphes :

Théorème

Si on sait résoudre 3-SAT alors on sait résoudre \(k\)-SAT pour tout \(k\).

Preuve

Une clause \(l_1 \vee \dots \vee l_p\) avec \(p > 3\) est remplacée par \((l_1 \vee l_2 \vee Z) \wedge (\neg Z \vee l_3 \vee \dots \vee l_p)\) où \(Z\) est une variable nouvelle. Les deux formules ne sont pas équivalentes mais sont équisatisfiables : un modèle de la clause initiale se prolonge en un modèle de la nouvelle formule (on pose \(v(Z) = F\) si \(l_1\) ou \(l_2\) est vrai, \(v(Z) = V\) sinon) et réciproquement un modèle de la nouvelle formule rend vrai l'un des \(l_i\) (si \(v(Z) = V\), c'est l'un de \(l_3, \dots, l_p\), sinon l'un de \(l_1, l_2\)). La seconde clause est plus courte d'un littéral : en itérant, on obtient une formule de 3-SAT équisatisfiable, de taille polynomiale en celle de la formule initiale.

Cependant, comme on en reparlera dans le chapitre sur la NP-complétude, le problème 3-SAT est a priori très difficile et on a peu d'espoir de pouvoir le résoudre de manière générale autrement qu'en énumérant les \(2^n\) valuations.

Algorithme de Quine

L'algorithme de Quine consiste à construire un arbre de décision associé à une formule \(f\) inductivement ainsi :

• si \(f\) est sans variable, \(f \equiv \top\) ou \(\perp\) et on renvoie une feuille avec cette valeur.
• sinon on considère une variable \(X\) quelconque dans \(f\) et on renvoie l'arbre dont la racine est étiquetée par \(X\), a pour fils gauche l'arbre associé à \(f[\top/X]\) et pour fils droit l'arbre associé à \(f[\perp/X]\).

Si \(f\) est satisfiable, alors cet arbre a une feuille de valeur \(\top\). Il suffit alors de lire les embranchements pour retrouver le modèle correspondant.

Si \(f\) est une tautologie, toutes ses feuilles sont étiquetées par \(\top\).

On donne ici une implémentation rapide de cet algorithme :

type formule = Et of formule * formule 
   | Ou of formule * formule | Non of formule 
   | Vrai | Faux | Var of string

let rec var f =
    match f with
    | Ou(f1, f2)
    | Et(f1, f2) -> var f1 @ var f2
    | Non f' -> var f'
    | Var s -> [s]
    | _ -> []

let rec subst f s v =
    match f with
    | Ou(f1, f2) -> Ou(subst f1 s v, subst f2 s v)
    | Et(f1, f2) -> Et(subst f1 s v, subst f2 s v)
    | Non f' -> Non (subst f' s v)
    | Var t when s = t -> v
    | _ -> f


let rec simpl f =
    match f with
    | Et(f1, f2) -> begin
            match simpl f1, simpl f2 with
            | Vrai, f -> f
            | f, Vrai -> f
            | Faux, _ -> Faux
            | _, Faux -> Faux
            | f1', f2' -> Et(f1', f2')
            end
    | Ou(f1, f2) -> begin
            match simpl f1, simpl f2 with
            | Vrai, _ -> Vrai
            | _, Vrai -> Vrai
            | Faux, f -> f
            | f, Faux -> f
            | f1', f2' -> Ou(f1', f2')
             end
    | Non f -> begin
        match simpl f with
        | Vrai -> Faux
        | Faux -> Vrai
        | f' -> Non f'
        end
    | _ -> f

type quine_resultat = Valide | Invalide | Branchement of string * quine_resultat * quine_resultat

let rec quine f =
    match simpl f with
    | Vrai -> Valide
    | Faux -> Invalide
    | f' -> let s = List.hd (var f') in
        Branchement(s, quine (subst f' s Vrai), quine (subst f' s Faux))

let imp f1 f2 = Ou(Non f1, f2)

let ex = imp (Et(Et(imp (Var "s") (Ou(Var "b", Var "t")), 
    imp (Ou(Var "b", Var "a"))  (Et(Var "r", Var "m"))), Non (Var "r")))
    (imp (Var "s") (Var "t"))

let b = quine ex