La logique propositionnelle (ou calcul propositionnel) constitue le niveau fondamental de la logique mathématique et fournit l'appareil formel nécessaire à l'analyse rigoureuse du raisonnement déductif. Elle étudie les propositions, c'est-à-dire les énoncés déclaratifs auxquels on peut associer de manière univoque une valeur de vérité, ainsi que leurs combinaisons à l'aide des connecteurs logiques.
Le présent exposé se veut systématique et complet : langage formel, syntaxe, sémantique vérifonctionnelle, équivalences et lois fondamentales, tautologies et conséquence logique, formes normales, systèmes déductifs, ainsi que les théorèmes métalogiques de correction et de complétude.
Sommaire
- Propositions et langage formel
- Syntaxe des formules bien formées
- Sémantique et interprétations
- Connecteurs logiques et complétude fonctionnelle
- Tables de vérité
- Équivalences logiques
- Lois fondamentales
- Tautologies, satisfiabilité et conséquence logique
- Formes normales (FNC et FND)
- Systèmes déductifs
- Correction et complétude
- Exemples développés
Propositions et langage formel
Une proposition (ou énoncé) est une phrase déclarative dotée d'un sens qui, en vertu du principe de bivalence, prend de manière univoque exactement l'une des deux valeurs de vérité : vrai (\(V\) ou \(1\)) ou faux (\(F\) ou \(0\)).
Une proposition est dite atomique (ou énoncé simple) si elle ne contient pas d'autre proposition reliée par un opérateur logique. Les propositions obtenues en combinant des propositions atomiques au moyen de connecteurs logiques sont dites composées (ou moléculaires).
On fixe un ensemble dénombrable de variables propositionnelles, généralement notées par des lettres latines minuscules :
\[ \mathcal{P} = \{p_1, p_2, p_3, \dots\} = \{p, q, r, \dots\} \]
Le langage de la logique propositionnelle \(\mathcal{L}\) est constitué des symboles suivants :
- les variables propositionnelles de \(\mathcal{P}\) ;
- les connecteurs logiques : \(\neg,\ \land,\ \lor,\ \rightarrow,\ \leftrightarrow\) ;
- les symboles auxiliaires : les parenthèses \((,\ )\).
Syntaxe des formules bien formées
L'ensemble \(\mathcal{F}\) des formules bien formées (fbf) est le plus petit ensemble de mots sur l'alphabet de \(\mathcal{L}\) défini par induction au moyen des clauses suivantes :
- Clause de base : toute variable propositionnelle \(p \in \mathcal{P}\) est une fbf ;
- Clauses inductives :
- si \(A \in \mathcal{F}\), alors \((\neg A) \in \mathcal{F}\) ;
- si \(A, B \in \mathcal{F}\), alors \((A \land B),\ (A \lor B),\ (A \rightarrow B),\ (A \leftrightarrow B) \in \mathcal{F}\) ;
- Clause de clôture : aucune autre chaîne de caractères n'est une fbf.
En notation BNF, la grammaire du langage s'écrit :
\[ A ::= p \mid (\neg A) \mid (A \land A) \mid (A \lor A) \mid (A \rightarrow A) \mid (A \leftrightarrow A) \]
Par convention de priorité, on attribue aux connecteurs l'ordre décroissant suivant, qui permet d'omettre les parenthèses sans ambiguïté :
\[ \neg \;>\; \land \;>\; \lor \;>\; \rightarrow \;>\; \leftrightarrow \]
Mise en garde. Si la priorité de \(\neg\) sur tous les autres connecteurs ainsi que la moindre priorité de \(\rightarrow\) et \(\leftrightarrow\) font l'objet d'un consensus universel, l'ordre relatif de \(\land\) et \(\lor\) n'est pas uniforme dans la littérature : certains auteurs (par analogie avec \(\cdot\) et \(+\) en algèbre de Boole) accordent à \(\land\) une priorité supérieure à \(\lor\), tandis que d'autres (par exemple Mendelson) les placent au même niveau et exigent des parenthèses explicites. Il est donc d'usage prudent, en cas d'ambiguïté possible, d'expliciter les parenthèses entre \(\land\) et \(\lor\) : on écrira par exemple \( (A \land B) \lor C \) plutôt que \( A \land B \lor C \).
Le principe d'induction structurelle sur les fbf affirme que, pour démontrer une propriété \(P\) pour toute \(A \in \mathcal{F}\), il suffit d'établir :
- (cas de base) \(P\) est vraie pour toute proposition atomique ;
- (pas inductif) \(P\) est préservée par l'application de chaque connecteur.
Sémantique et interprétations
La sémantique de la logique propositionnelle est vérifonctionnelle : la valeur de vérité d'une formule composée est entièrement déterminée par les valeurs de vérité de ses sous-formules.
Une interprétation (ou valuation, ou distribution de valeurs de vérité) est une fonction :
\[ v : \mathcal{P} \to \{V, F\} \]
qui s'étend de manière unique en une fonction \(\hat{v} : \mathcal{F} \to \{V, F\}\) au moyen des clauses récursives suivantes :
- \( \hat{v}(\neg A) = V \iff \hat{v}(A) = F \) ;
- \( \hat{v}(A \land B) = V \iff \hat{v}(A) = V \text{ et } \hat{v}(B) = V \) ;
- \( \hat{v}(A \lor B) = V \iff \hat{v}(A) = V \text{ ou } \hat{v}(B) = V \) (éventuellement les deux) ;
- \( \hat{v}(A \rightarrow B) = F \iff \hat{v}(A) = V \text{ et } \hat{v}(B) = F \) ;
- \( \hat{v}(A \leftrightarrow B) = V \iff \hat{v}(A) = \hat{v}(B) \).
Si une formule contient \(n\) variables propositionnelles distinctes, le nombre d'interprétations possibles (restreintes à ces variables) est \(2^n\).
Remarque importante. Le connecteur \(\lor\) représente la disjonction inclusive (correspondant au vel latin) : \(A \lor B\) est vraie dès qu'au moins l'une des deux propositions est vraie, y compris lorsqu'elles sont vraies toutes les deux. Il faut la distinguer de la disjonction exclusive (correspondant à l'aut latin, notée \(\oplus\) ou XOR), pour laquelle \(A \oplus B\) est vraie si et seulement si \(A\) et \(B\) ont des valeurs de vérité différentes. Symboliquement :
\[ A \oplus B \;\equiv\; (A \lor B) \land \neg(A \land B) \;\equiv\; \neg(A \leftrightarrow B) \]
Dans le langage courant, le « ou » français est ambigu entre les deux lectures ; la logique formelle lève cette ambiguïté en adoptant par défaut la lecture inclusive.
Connecteurs logiques et complétude fonctionnelle
Les connecteurs logiques sont des opérateurs vérifonctionnels, c'est-à-dire des fonctions \(\{V,F\}^n \to \{V,F\}\) :
- la négation \(\neg\) est un opérateur unaire ;
- la conjonction \(\land\), la disjonction \(\lor\), l'implication (ou conditionnel) \(\rightarrow\) et l'équivalence (ou biconditionnel) \(\leftrightarrow\) sont des opérateurs binaires.
Un ensemble de connecteurs est dit fonctionnellement complet (ou adéquat) si toute fonction de vérité \(\{V,F\}^n \to \{V,F\}\) peut s'exprimer comme combinaison de ces connecteurs. Sont fonctionnellement complets, par exemple :
\[ \{\neg, \land, \lor\}, \quad \{\neg, \land\}, \quad \{\neg, \lor\}, \quad \{\neg, \rightarrow\} \]
De plus, certains connecteurs binaires sont à eux seuls fonctionnellement complets : la barre de Sheffer (NAND), notée \(\uparrow\), et la flèche de Peirce (NOR), notée \(\downarrow\).
Les définitions sémantiques justifient les réductions suivantes, qui montrent que \(\rightarrow\) et \(\leftrightarrow\) sont définissables à partir de \(\{\neg, \land, \lor\}\) :
\[ A \rightarrow B \equiv \neg A \lor B \]
\[ A \leftrightarrow B \equiv (A \rightarrow B) \land (B \rightarrow A) \equiv (A \land B) \lor (\neg A \land \neg B) \]
Tables de vérité
Une table de vérité est la représentation tabulaire de la fonction vérifonctionnelle associée à une formule. Pour une formule contenant \(n\) variables distinctes, la table comporte \(2^n\) lignes, une pour chaque interprétation possible.
Les tables de vérité des connecteurs fondamentaux sont les suivantes :
| \(A\) | \(B\) | \(\neg A\) | \(A \land B\) | \(A \lor B\) | \(A \rightarrow B\) | \(A \leftrightarrow B\) |
|---|---|---|---|---|---|---|
| V | V | F | V | V | V | V |
| V | F | F | F | V | F | F |
| F | V | V | F | V | V | F |
| F | F | V | F | F | V | V |
On observera que l'implication \(A \rightarrow B\) est fausse uniquement lorsque l'antécédent \(A\) est vrai et le conséquent \(B\) faux : c'est l'unique ligne où elle prend la valeur \(F\).
Équivalences logiques
Deux formules \(A\) et \(B\) sont dites logiquement équivalentes, ce que l'on note \(A \equiv B\), si elles prennent la même valeur de vérité dans toute interprétation :
\[ A \equiv B \iff \forall v,\ \hat{v}(A) = \hat{v}(B) \]
La relation \(\equiv\) est une relation d'équivalence sur \(\mathcal{F}\) (réflexive, symétrique, transitive) et une congruence : le théorème de remplacement énonce que si \(A \equiv B\) et que \(C[A]\) est une formule contenant \(A\) comme sous-formule, alors \(C[A] \equiv C[B]\), où \(C[B]\) est obtenue en remplaçant (une occurrence de) \(A\) par \(B\) dans \(C\).
Il est essentiel de distinguer \(\equiv\) (relation métalinguistique entre formules) du connecteur \(\leftrightarrow\) (qui appartient au langage objet) ; on a en effet
\[ A \equiv B \iff \models A \leftrightarrow B \]
autrement dit, \(A\) et \(B\) sont logiquement équivalentes si et seulement si \(A \leftrightarrow B\) est une tautologie.
Lois fondamentales
Les équivalences suivantes, toutes démontrables au moyen de tables de vérité, constituent les lois fondamentales du calcul propositionnel (\(\top\) désigne ici une tautologie quelconque, \(\bot\) une contradiction) :
- Idempotence : \(A \land A \equiv A\), \(\quad A \lor A \equiv A\)
- Commutativité : \(A \land B \equiv B \land A\), \(\quad A \lor B \equiv B \lor A\)
- Associativité : \((A \land B) \land C \equiv A \land (B \land C)\), et de même pour \(\lor\)
- Distributivité : \(A \land (B \lor C) \equiv (A \land B) \lor (A \land C)\), \(\quad A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)\)
- Double négation : \(\neg \neg A \equiv A\)
- Lois de De Morgan : \(\neg(A \land B) \equiv \neg A \lor \neg B\), \(\quad \neg(A \lor B) \equiv \neg A \land \neg B\)
- Absorption : \(A \land (A \lor B) \equiv A\), \(\quad A \lor (A \land B) \equiv A\)
- Élément neutre : \(A \land \top \equiv A\), \(\quad A \lor \bot \equiv A\)
- Élément absorbant : \(A \lor \top \equiv \top\), \(\quad A \land \bot \equiv \bot\)
- Tiers exclu : \(A \lor \neg A \equiv \top\)
- Non-contradiction : \(A \land \neg A \equiv \bot\)
- Contraposition : \(A \rightarrow B \equiv \neg B \rightarrow \neg A\)
- Exportation : \((A \land B) \rightarrow C \equiv A \rightarrow (B \rightarrow C)\)
Tautologies, satisfiabilité et conséquence logique
Soit \(A \in \mathcal{F}\). On dit que :
- \(A\) est une tautologie (ou formule logiquement valide), ce que l'on note \(\models A\), si \(\hat{v}(A) = V\) pour toute interprétation \(v\) ;
- \(A\) est une contradiction (ou formule insatisfiable) si \(\hat{v}(A) = F\) pour tout \(v\) ;
- \(A\) est satisfiable s'il existe au moins une interprétation \(v\) telle que \(\hat{v}(A) = V\) ;
- \(A\) est contingente si elle est satisfiable mais n'est pas une tautologie.
Les quatre catégories sont liées par la dualité :
\[ A \text{ est une tautologie} \iff \neg A \text{ est une contradiction} \]
Soient \(\Gamma \subseteq \mathcal{F}\) un ensemble de formules (éventuellement infini) et \(B \in \mathcal{F}\). On dit que \(B\) est conséquence logique (sémantique) de \(\Gamma\), ce que l'on note
\[ \Gamma \models B \]
si pour toute interprétation \(v\) telle que \(\hat{v}(A) = V\) pour tout \(A \in \Gamma\), on a \(\hat{v}(B) = V\). Autrement dit : tout modèle de \(\Gamma\) est un modèle de \(B\).
Théorème de déduction sémantique :
\[ \Gamma \cup \{A\} \models B \iff \Gamma \models A \rightarrow B \]
En particulier, en prenant \(\Gamma = \emptyset\), on obtient \(A \models B\) si et seulement si \(\models A \rightarrow B\).
Formes normales (FNC et FND)
On appelle littéral une variable propositionnelle ou sa négation : \(p\) ou \(\neg p\). Par conséquent :
- une clause disjonctive est une disjonction de littéraux : \(\ell_1 \lor \ell_2 \lor \dots \lor \ell_k\) ;
- une clause conjonctive est une conjonction de littéraux : \(\ell_1 \land \ell_2 \land \dots \land \ell_k\).
Une formule est en :
- Forme Normale Conjonctive (FNC) si elle est une conjonction de clauses disjonctives ;
- Forme Normale Disjonctive (FND) si elle est une disjonction de clauses conjonctives.
Théorème (existence des formes normales). Toute formule \(A \in \mathcal{F}\) est logiquement équivalente à une formule en FNC et à une formule en FND.
Procédure de réduction :
- éliminer le biconditionnel : \(A \leftrightarrow B \equiv (A \rightarrow B) \land (B \rightarrow A)\) ;
- éliminer l'implication : \(A \rightarrow B \equiv \neg A \lor B\) ;
- faire descendre les négations jusqu'aux variables (lois de De Morgan et double négation), obtenant ainsi la forme normale négative (FNN) ;
- appliquer la distributivité pour obtenir la forme désirée : \(\lor\) sur \(\land\) pour la FND, \(\land\) sur \(\lor\) pour la FNC.
Exemple :
\[ A \rightarrow (B \lor C) \;\equiv\; \neg A \lor (B \lor C) \;\equiv\; \neg A \lor B \lor C \]
qui est à la fois en FNC (une unique clause disjonctive) et en FND (une disjonction de clauses conjonctives réduites à des littéraux uniques).
Systèmes déductifs
Un système déductif (ou calcul logique) est un dispositif purement syntaxique constitué d'axiomes et de règles d'inférence, qui permet de dériver des formules à partir de prémisses sans recours à la sémantique. La notion fondamentale est celle de dérivabilité : on note
\[ \Gamma \vdash A \]
pour signifier qu'il existe une dérivation de la formule \(A\) à partir des prémisses \(\Gamma\) dans le système considéré.
Les systèmes déductifs les plus répandus pour la logique propositionnelle sont :
- Systèmes axiomatiques (à la Hilbert-Frege) : peu de schémas d'axiomes et une seule règle d'inférence (le modus ponens) ;
- Déduction naturelle (Gentzen, Prawitz) : règles d'introduction et d'élimination pour chaque connecteur ;
- Calcul des séquents (Gentzen) : règles agissant sur des séquents \(\Gamma \Rightarrow \Delta\) ;
- Tableaux sémantiques (Beth, Smullyan) : méthode de réfutation par arbres.
Les règles d'inférence les plus importantes sont :
Modus Ponens (élimination de \(\rightarrow\)) :
\[ \dfrac{A \qquad A \rightarrow B}{B} \]
Modus Tollens (règle de la contraposée) :
\[ \dfrac{A \rightarrow B \qquad \neg B}{\neg A} \]
Syllogisme hypothétique (transitivité de l'implication) :
\[ \dfrac{A \rightarrow B \qquad B \rightarrow C}{A \rightarrow C} \]
Syllogisme disjonctif :
\[ \dfrac{A \lor B \qquad \neg A}{B} \]
Introduction et élimination de la conjonction :
\[ \dfrac{A \qquad B}{A \land B} \qquad\qquad \dfrac{A \land B}{A} \qquad\qquad \dfrac{A \land B}{B} \]
Raisonnement par l'absurde :
\[ \dfrac{\Gamma, \neg A \vdash \bot}{\Gamma \vdash A} \]
Correction et complétude
La relation entre la dérivabilité syntaxique \(\vdash\) et la conséquence sémantique \(\models\) est exprimée par les deux théorèmes métalogiques fondamentaux de la logique propositionnelle.
Théorème de correction. Pour tout \(\Gamma \subseteq \mathcal{F}\) et tout \(A \in \mathcal{F}\) :
\[ \Gamma \vdash A \;\Longrightarrow\; \Gamma \models A \]
Tout ce qui est dérivable syntaxiquement est effectivement conséquence sémantique des prémisses.
Théorème de complétude (Post, 1921). Pour tout \(\Gamma \subseteq \mathcal{F}\) et tout \(A \in \mathcal{F}\) :
\[ \Gamma \models A \;\Longrightarrow\; \Gamma \vdash A \]
Toute conséquence sémantique peut effectivement être dérivée dans le calcul.
En combinant les deux résultats, on obtient l'équivalence entre syntaxe et sémantique :
\[ \Gamma \vdash A \iff \Gamma \models A \]
À ces résultats s'ajoutent deux autres énoncés métalogiques d'importance :
- Théorème de compacité : \(\Gamma\) est satisfiable si et seulement si toute partie finie de \(\Gamma\) est satisfiable ;
- Décidabilité : il existe un algorithme (par exemple la méthode des tables de vérité) qui, en un nombre fini d'étapes, décide si une formule donnée est ou non une tautologie.
Exemples développés
Exemple 1 — Réduction en forme normale
Réduire \( (A \rightarrow B) \land \neg B \) en FNC et en FND.
Résultat
FNC : \( (\neg A \lor B) \land \neg B \) — FND : \( \neg A \land \neg B \)
Résolution
On élimine l'implication grâce à \( A \rightarrow B \equiv \neg A \lor B \) :
\[ (A \rightarrow B) \land \neg B \;\equiv\; (\neg A \lor B) \land \neg B \]
ce qui est déjà en FNC (conjonction de deux clauses disjonctives). Pour obtenir la FND, on distribue \(\land\) sur \(\lor\) :
\[ (\neg A \lor B) \land \neg B \;\equiv\; (\neg A \land \neg B) \lor (B \land \neg B) \;\equiv\; \neg A \land \neg B \]
puisque \( B \land \neg B \equiv \bot \) en vertu de la loi de non-contradiction. Le résultat \( \neg A \land \neg B \) est une FND dégénérée : il s'agit en effet d'une unique clause conjonctive, que l'on peut interpréter comme une disjonction réduite à un seul terme. Par convention, une clause conjonctive isolée est considérée comme étant en FND (de même qu'une clause disjonctive isolée est en FNC), bien qu'aucun \(\lor\) n'y apparaisse explicitement.
Exemple 2 — Vérification d'une tautologie (syllogisme hypothétique)
Montrer que \( ((A \rightarrow B) \land (B \rightarrow C)) \rightarrow (A \rightarrow C) \) est une tautologie.
Résolution
On raisonne par l'absurde : supposons qu'il existe une interprétation \(v\) sous laquelle la formule est fausse. Pour qu'une implication soit fausse, son antécédent doit être vrai et son conséquent faux ; on en déduit :
- \( \hat{v}((A \rightarrow B) \land (B \rightarrow C)) = V \), donc \( \hat{v}(A \rightarrow B) = V \) et \( \hat{v}(B \rightarrow C) = V \) ;
- \( \hat{v}(A \rightarrow C) = F \), d'où \( \hat{v}(A) = V \) et \( \hat{v}(C) = F \).
De \( \hat{v}(A) = V \) et \( \hat{v}(A \rightarrow B) = V \) on tire \( \hat{v}(B) = V \) (sinon l'implication serait fausse). De \( \hat{v}(B) = V \) et \( \hat{v}(B \rightarrow C) = V \) il vient \( \hat{v}(C) = V \), en contradiction avec \( \hat{v}(C) = F \). La formule est donc une tautologie.
Exemple 3 — Conséquence logique et règle de résolution
Vérifier que \( \{A \lor B,\ \neg A \lor C\} \models B \lor C \).
Résolution
Soit \(v\) une interprétation satisfaisant les deux prémisses. On distingue deux cas selon la valeur de \( \hat{v}(A) \) :
- si \( \hat{v}(A) = V \), alors de \( \hat{v}(\neg A \lor C) = V \) on tire nécessairement \( \hat{v}(C) = V \), d'où \( \hat{v}(B \lor C) = V \) ;
- si \( \hat{v}(A) = F \), alors de \( \hat{v}(A \lor B) = V \) on tire \( \hat{v}(B) = V \), d'où \( \hat{v}(B \lor C) = V \).
Dans les deux cas \( \hat{v}(B \lor C) = V \), ce qui prouve la conséquence logique. Ce principe constitue la règle de résolution, pierre angulaire des méthodes de démonstration automatique : à partir des clauses \( A \lor B \) et \( \neg A \lor C \), on déduit le résolvant \( B \lor C \).
La logique propositionnelle représente le premier niveau de formalisation du raisonnement mathématique. Malgré son pouvoir expressif limité — elle ne permet pas de décrire la structure interne des propositions —, elle fournit les outils conceptuels fondamentaux pour aborder la logique du premier ordre, les théories axiomatiques, la métalogique et les structures algébriques associées (algèbres de Boole, treillis). Sa maîtrise est un prérequis indispensable à toute étude rigoureuse des mathématiques et de l'informatique théorique.