Logique formelle
Propositions, prédicats, déduction, incomplétude — la structure du raisonnement mathématique mise à nu.
§ 1 Propositions et connecteurs logiques
Une proposition (ou formule close) est un énoncé qui est soit vrai (1) soit faux (0). Les variables propositionnelles $P, Q, R, \ldots$ représentent des propositions atomiques.
| Connecteur | Symbole | Lecture | Vrai quand |
|---|---|---|---|
| Négation | $\lnot P$ | non $P$ | $P$ est faux |
| Conjonction | $P\land Q$ | $P$ et $Q$ | $P$ et $Q$ vrais |
| Disjonction | $P\lor Q$ | $P$ ou $Q$ | Au moins l'un vrai |
| Implication | $P\Rightarrow Q$ | $P$ implique $Q$ | $P$ faux, ou $Q$ vrai |
| Équivalence | $P\Leftrightarrow Q$ | $P$ ssi $Q$ | Même valeur de vérité |
| OU exclusif | $P\oplus Q$ | $P$ xor $Q$ | Exactement l'un vrai |
| NAND | $P\uparrow Q$ | non-et | Pas les deux vrais |
| NOR | $P\downarrow Q$ | non-ou | Les deux faux |
De la plus haute à la plus basse priorité : $\lnot$, $\land$, $\lor$, $\Rightarrow$, $\Leftrightarrow$. Ainsi $\lnot P\land Q\Rightarrow R$ se lit $(\lnot P)\land Q)\Rightarrow R$.
§ 2 Tables de vérité
| $P$ | $Q$ | $\lnot P$ | $P\land Q$ | $P\lor Q$ | $P\Rightarrow Q$ | $P\Leftrightarrow Q$ | $P\oplus Q$ |
|---|---|---|---|---|---|---|---|
| 0 | 0 | 1 | 0 | 0 | 1 | 1 | 0 |
| 0 | 1 | 1 | 0 | 1 | 1 | 0 | 1 |
| 1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 |
| 1 | 1 | 0 | 1 | 1 | 1 | 1 | 0 |
$P\Rightarrow Q$ est faux uniquement quand $P$ est vrai et $Q$ est faux. L'implication "ex falso quodlibet" : une prémisse fausse rend l'implication vraie quelle que soit la conclusion. Ainsi "$1=2\Rightarrow$ la Lune est en fromage" est une proposition vraie en logique classique.
Une formule à $n$ variables propositionnelles a $2^n$ lignes dans sa table de vérité. Pour $n=3$ variables $P,Q,R$ : $2^3=8$ lignes. On remplit les colonnes de droite à gauche en alternant : $R$ change à chaque ligne, $Q$ change toutes les 2 lignes, $P$ toutes les 4.
§ 3 Tautologies, contradictions, équivalences
- Tautologie : formule vraie pour toute valuation ($\models \varphi$)
- Contradiction : formule fausse pour toute valuation
- Satisfaisable : vraie pour au moins une valuation
- Contingente : ni tautologie ni contradiction
| Nom | Formule |
|---|---|
| Tiers exclu | $P\lor\lnot P$ |
| Non-contradiction | $\lnot(P\land\lnot P)$ |
| Double négation | $P\Leftrightarrow\lnot\lnot P$ |
| Modus ponens | $(P\land(P\Rightarrow Q))\Rightarrow Q$ |
| Modus tollens | $(\lnot Q\land(P\Rightarrow Q))\Rightarrow\lnot P$ |
| Syllogisme hypothétique | $((P\Rightarrow Q)\land(Q\Rightarrow R))\Rightarrow(P\Rightarrow R)$ |
| Dilemme constructif | $((P\Rightarrow R)\land(Q\Rightarrow R)\land(P\lor Q))\Rightarrow R$ |
| Contraposée | $(P\Rightarrow Q)\Leftrightarrow(\lnot Q\Rightarrow\lnot P)$ |
§ 4 Formes normales
- Littéral : variable propositionnelle ou sa négation ($P$ ou $\lnot P$)
- Clause : disjonction de littéraux ($P\lor\lnot Q\lor R$)
- Terme : conjonction de littéraux ($P\land\lnot Q\land R$)
- FNC (Forme Normale Conjonctive) : conjonction de clauses. Exemple : $(P\lor Q)\land(\lnot P\lor R)\land(Q\lor\lnot R)$
- FND (Forme Normale Disjonctive) : disjonction de termes. Exemple : $(P\land Q)\lor(\lnot P\land R)$
- Toute formule est équivalente à une FNC et à une FND.
- Éliminer $\Leftrightarrow$ : $A\Leftrightarrow B \equiv (A\Rightarrow B)\land(B\Rightarrow A)$
- Éliminer $\Rightarrow$ : $A\Rightarrow B \equiv \lnot A\lor B$
- Pousser les négations vers les atomes (De Morgan, double négation)
- Distribuer $\land$ sur $\lor$
Tout connecteur booléen peut s'exprimer avec $\{\lnot, \land\}$, avec $\{\lnot, \lor\}$, avec $\{\mathrm{NAND}\}$, ou avec $\{\mathrm{NOR}\}$. Ces ensembles sont dits fonctionnellement complets.
Le problème SAT demande : étant donné une formule en FNC, existe-t-il une valuation qui la satisfait ? SAT est le premier problème démontré NP-complet (Cook-Levin, 1971). Le problème 2-SAT (clauses à 2 littéraux) est en P ; 3-SAT est NP-complet.
§ 5 Calcul des prédicats (logique du premier ordre)
Un prédicat $P(x)$ est une propriété paramétrique. Les quantificateurs lient les variables :
- $\forall x\, P(x)$ : "pour tout $x$, $P(x)$" (quantificateur universel)
- $\exists x\, P(x)$ : "il existe $x$ tel que $P(x)$" (quantificateur existentiel)
- $\exists!\, x\, P(x)$ : "il existe un unique $x$ tel que $P(x)$"
Exemple : $\lnot(\forall\varepsilon>0,\exists\delta>0,\ldots) \equiv \exists\varepsilon>0,\forall\delta>0,\lnot(\ldots)$.
L'ordre des quantificateurs est crucial :
- $\forall x\,\exists y\, P(x,y)$ : pour tout $x$, on trouve un $y$ (qui peut dépendre de $x$)
- $\exists y\,\forall x\, P(x,y)$ : il existe un $y$ qui marche pour tous les $x$ (plus fort)
$\exists y\,\forall x\Rightarrow\forall x\,\exists y$ (réciproque fausse en général).
Syntaxe du premier ordre : termes (variables, constantes, fonctions) ; formules atomiques ($P(t_1,\ldots,t_n)$, $t_1=t_2$) ; formules construites par $\lnot,\land,\lor,\Rightarrow,\Leftrightarrow,\forall,\exists$. Une variable est libre si non liée par un quantificateur, sinon liée.
Un énoncé du premier ordre est prouvable dans le calcul des prédicats si et seulement s'il est vrai dans tout modèle. Autrement dit : $\vdash\varphi \Leftrightarrow \models\varphi$ (la déductibilité coïncide avec la validité sémantique).
§ 6 Systèmes de déduction
Un séquent $\Gamma\vdash\Delta$ exprime que si toutes les formules de $\Gamma$ sont vraies, alors au moins l'une de $\Delta$ est vraie. Règles structurelles : affaiblissement, contraction, permutation, coupure.
| Règle | Introduction | Élimination |
|---|---|---|
| $\land$ | $\dfrac{A\quad B}{A\land B}$ | $\dfrac{A\land B}{A}$, $\dfrac{A\land B}{B}$ |
| $\lor$ | $\dfrac{A}{A\lor B}$, $\dfrac{B}{A\lor B}$ | $\dfrac{A\lor B\quad [A]\vdash C\quad [B]\vdash C}{C}$ |
| $\Rightarrow$ | $\dfrac{[A]\vdash B}{A\Rightarrow B}$ | $\dfrac{A\Rightarrow B\quad A}{B}$ (MP) |
| $\lnot$ | $\dfrac{[A]\vdash\bot}{\lnot A}$ | $\dfrac{\lnot A\quad A}{\bot}$ |
| $\forall$ | $\dfrac{A[x/t]}{\forall x\, A}$ ($x$ non libre) | $\dfrac{\forall x\, A}{A[x/t]}$ |
| $\exists$ | $\dfrac{A[x/t]}{\exists x\, A}$ | $\dfrac{\exists x\, A\quad [A[x/c]]\vdash B}{B}$ ($c$ fraîche) |
Dans le calcul des séquents LK (classique), toute preuve peut être transformée en preuve sans coupure (cut-free). Ce théorème dit que la coupure est une règle dérivée, pas primitive. Il entraîne la propriété de la sous-formule : chaque formule d'une preuve sans coupure est sous-formule de la conclusion.
§ 7 Théorèmes d'incomplétude de Gödel
On encode chaque symbole, formule et preuve par un entier naturel (son numéro de Gödel $\ulcorner\varphi\urcorner$). Cela permet d'exprimer des méta-énoncés logiques (comme "la formule $n$ est prouvable") sous forme d'énoncés arithmétiques.
Toute théorie formelle $T$ cohérente, récursivement axiomatisable et suffisamment expressive (contenant l'arithmétique de Peano) est incomplète : il existe un énoncé $G_T$ tel que ni $T\vdash G_T$ ni $T\vdash\lnot G_T$.
$G_T$ est l'énoncé "je ne suis pas prouvable dans $T$" (construction diagonale). $G_T$ est vrai dans le modèle standard de $\mathbb{N}$, mais non prouvable.
Sous les mêmes hypothèses, $T$ ne peut pas prouver sa propre cohérence : $T\not\vdash\mathrm{Con}(T)$ (si $T$ est cohérente). On peut cependant prouver la cohérence de $T$ dans une théorie plus forte.
- Le programme de Hilbert (formaliser toutes les mathématiques) est impossible dans sa forme forte
- La vérité mathématique transcende la provabilité formelle
- Il existe une infinité de théories formelles différentes, toutes cohérentes et incomplètes
- Relation avec la calculabilité : l'indécidabilité du problème de l'arrêt de Turing (1936) est un analogue computationnel
Il n'existe pas de prédicat de vérité définissable dans $T$ : la vérité arithmétique $\mathrm{True}(n)$ ne peut pas être définie par une formule arithmétique (sinon, paradoxe du menteur formalisé). Ce théorème précède et renforce l'incomplétude de Gödel.
§ 8 Logiques non classiques et modales
La logique modale étend la logique classique avec les opérateurs :
- $\Box\varphi$ : "il est nécessaire que $\varphi$" (ou "toujours", "partout")
- $\Diamond\varphi$ : "il est possible que $\varphi$" (ou "parfois", "quelque part")
Relation : $\Diamond\varphi \equiv \lnot\Box\lnot\varphi$.
Un cadre de Kripke $(W, R)$ : $W$ ensemble de mondes, $R\subset W\times W$ relation d'accessibilité. Une formule $\Box\varphi$ est vraie en $w$ si $\varphi$ est vraie en tout $v$ tel que $wRv$.
| Système | Axiomes | Relation $R$ | Usage |
|---|---|---|---|
| K | $\Box(\varphi\Rightarrow\psi)\Rightarrow(\Box\varphi\Rightarrow\Box\psi)$ | Quelconque | Base |
| T | K + $\Box\varphi\Rightarrow\varphi$ | Réflexive | Nécessité |
| S4 | T + $\Box\varphi\Rightarrow\Box\Box\varphi$ | Réflexive + transitive | Topologie |
| S5 | S4 + $\Diamond\varphi\Rightarrow\Box\Diamond\varphi$ | Relation d'équivalence | Logique épistémique |
| GL | K + $\Box(\Box\varphi\Rightarrow\varphi)\Rightarrow\Box\varphi$ | Bien fondée + transitive | Provabilité (Solovay) |
- Logique intuitionniste : rejette le tiers exclu $P\lor\lnot P$. Preuves = constructions. Correspondance de Curry–Howard : preuves ↔ programmes.
- Logique linéaire (Girard) : les hypothèses sont des ressources à consommer. Connecteurs additifs et multiplicatifs distincts.
- Logique paraconsistante : tolère des contradictions sans trivialisés ($A\land\lnot A$ ne dérive pas tout).
- Logique floue (Zadeh) : valeurs de vérité dans $[0,1]$, pas seulement $\{0,1\}$.
Il existe une correspondance profonde entre :
| Logique | Informatique (types et programmes) |
|---|---|
| Proposition | Type |
| Preuve de $A$ | Programme de type $A$ |
| $A\Rightarrow B$ | Type fonction $A\to B$ |
| $A\land B$ | Type produit $A\times B$ |
| $A\lor B$ | Type somme $A+B$ |
| $\forall x, P(x)$ | Type dépendant $\Pi x:A, P(x)$ |
| Normalisation de preuve | Évaluation de programme |
Cette correspondance est à la base des assistants de preuve modernes (Coq, Agda, Lean).