Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter

Support de cours · chapitre 6

La déduction naturelle

Démontrer une formule par une suite de petits pas, chacun justifié par une règle, comme on raisonne à la main, et pourquoi ces preuves disent vrai.

Prouver plutôt que calculer

Jusqu'ici, pour savoir si $\Sigma \vDash A$, on calcule : tables de vérité, recherche de contre-modèle, résolution. Ces méthodes répondent, mais ne ressemblent pas à un raisonnement. La déduction naturelle (Gentzen, 1934) écrit des preuves : des suites de pas élémentaires, chacun justifié par une règle, qui ressemblent à ce qu'on écrirait dans une copie de mathématiques.

On note $\Sigma \vdash A$, et on lit « $A$ est prouvable à partir de $\Sigma$ », s'il existe une preuve de $A$ qui n'utilise que les hypothèses de $\Sigma$.

Deux symboles, deux notions :

  • $\Sigma \vDash A$ parle de vérité : tout modèle de $\Sigma$ est un modèle de $A$ ;
  • $\Sigma \vdash A$ parle de preuve : on sait écrire une démonstration.

Le théorème de la fin du chapitre dit qu'elles coïncident.

Les règles

Chaque connecteur a deux sortes de règles : une règle d'introduction ($i$), qui dit comment prouver une formule dont c'est le connecteur principal, et une règle d'élimination ($e$), qui dit comment utiliser une telle formule. Au-dessus du trait, ce qu'il faut avoir établi ; en dessous, ce qu'on en tire.

Conjonction

$$\frac{A \qquad B}{A \land B}\;(\land_i) \qquad\qquad \frac{A \land B}{A}\;(\land_{e1}) \qquad \frac{A \land B}{B}\;(\land_{e2})$$

Implication

$$\frac{\begin{matrix}[A] \\ \vdots \\ B\end{matrix}}{A \to B}\;(\to_i) \qquad\qquad \frac{A \to B \qquad A}{B}\;(\to_e)$$

Pour prouver $A \to B$, on suppose $A$, et on prouve $B$ sous cette hypothèse. Une fois $A \to B$ obtenue, l'hypothèse $A$ est déchargée : on ne peut plus s'en servir. C'est exactement « supposons $A$ ; … ; donc $B$ ; ainsi $A \to B$ ». L'élimination est le modus ponens.

Disjonction

$$\frac{A}{A \lor B}\;(\lor_{i1}) \qquad \frac{B}{A \lor B}\;(\lor_{i2}) \qquad\qquad \frac{A \lor B \qquad \begin{matrix}[A] \\ \vdots \\ C\end{matrix} \qquad \begin{matrix}[B] \\ \vdots \\ C\end{matrix}}{C}\;(\lor_e)$$

L'élimination est le raisonnement par cas : si $A$ ou $B$, et que $C$ découle de chacun des deux cas, alors $C$.

Négation et absurde

On traite $\lnot A$ comme « $A$ mène à une contradiction », notée $\bot$.

$$\frac{\begin{matrix}[A] \\ \vdots \\ \bot\end{matrix}}{\lnot A}\;(\lnot_i) \qquad \frac{A \qquad \lnot A}{\bot}\;(\lnot_e) \qquad \frac{\bot}{A}\;(\bot_e) \qquad \frac{\begin{matrix}[\lnot A] \\ \vdots \\ \bot\end{matrix}}{A}\;(\text{RAA})$$

$(\bot_e)$ dit que d'une contradiction on tire n'importe quoi. $(\text{RAA})$ est le raisonnement par l'absurde : pour prouver $A$, supposer $\lnot A$ et aboutir à une contradiction. C'est lui qui rend la logique classique ; sans lui, on ne peut pas prouver $p \lor \lnot p$.

L'équivalence $A \leftrightarrow B$ est une abréviation de $(A \to B) \land (B \to A)$.

Écrire une preuve

On écrit la preuve comme une liste numérotée, dite à la Fitch. Une hypothèse provisoire ouvre une boîte, marquée par un trait vertical ; la règle qui la décharge ferme la boîte. On ne peut utiliser une ligne que tant qu'on n'est pas sorti de sa boîte. À l'intérieur d'une boîte, on peut recopier une ligne d'une boîte extérieure encore ouverte : c'est la réitération.

Preuve et vérité

Théorème. Pour tout ensemble de formules $\Sigma$ et toute formule $A$ :

  • correction : si $\Sigma \vdash A$, alors $\Sigma \vDash A$ ;
  • complétude : si $\Sigma \vDash A$, alors $\Sigma \vdash A$.

La correction se démontre règle par règle : chacune, appliquée à des formules vraies dans une interprétation, produit une formule vraie dans cette interprétation (en tenant compte des hypothèses déchargées). Par exemple, pour $(\to_e)$ : si $A \to B$ et $A$ sont vraies dans $v$, alors $B$ l'est. La complétude est plus difficile, et admise.

Conséquence : pour montrer qu'une formule n'est pas prouvable, il suffit d'un contre-modèle. On ne prouvera jamais $p \to q$ sans hypothèse, puisque $p = 1, q = 0$ la rend fausse.