Déduction naturelle

Cours complet · informatique (MP2I/MPI), chapitre 28 · MP2I et MPI

Travailler ce chapitre sur Adloun Exercices corrigés de ce chapitre

28.1 Pourquoi les tables de vérité ne suffisent pas

Le chapitre chap:logique savait déjà décider si une formule est une tautologie : on dresse sa table de vérité. Le programme explique pourquoi cela ne suffit pas, et il donne deux raisons.

ImportantLes deux défauts que la déduction naturelle vient corriger

« Il s'agit de présenter les preuves comme permettant de pallier deux problèmes de la présentation précédente du calcul propositionnel : nature exponentielle de la vérification d'une tautologie, faible lien avec les preuves mathématiques. »

Le coût. Une formule à $n$ variables a $2^{n}$ lignes de table. À $n = 60$ , il y a plus de lignes que de secondes depuis le Big Bang. Une preuve, elle, peut tenir en dix lignes quelle que soit $n$ .
La forme. Aucun mathématicien ne démontre par table de vérité. On suppose, on déduit, on conclut. La déduction naturelle formalise exactement ces gestes — d'où son nom.

AttentionCe que le programme attend, et ce qu'il proscrit

Deux phrases cadrent tout le chapitre : « il ne s'agit pas d'implémenter ces règles mais plutôt d'être capable d'écrire de petites preuves dans ce système », et « toute technicité dans les preuves dans ce système est à proscrire ».

On apprend donc à lire et à écrire des arbres de preuve de quelques nœuds. On ne démontre ni la complétude, ni l'élimination des coupures, et l'on ne code aucun vérificateur.

28.2 Séquents et règles d'inférence

Définition 28.1Séquent

Un séquent s'écrit

$H_{1}, \dots, H_{n} ⊢ C$

et se lit : « des hypothèses $H_{1}, \dots, H_{n}$ , on déduit $C$ ». La partie gauche est le contexte, souvent noté $Γ$ .

Important

⊢

⊨

ne disent pas la même chose

C'est la distinction syntaxe/sémantique du chapitre chap:logique, à son point le plus net.

	$Γ ⊨ C$	$Γ ⊢ C$
Nature	sémantique	syntaxique
Ce que cela dit	tout modèle de $Γ$ l'est de $C$	il existe une dérivation de $C$
Comment on l'établit	en examinant les valuations	en construisant un arbre
Coût	$2^{n}$ lignes	la taille de la preuve

Le premier parle de vérité, le second de démontrabilité. Rien n'oblige a priori les deux à coïncider — c'est un théorème, et il a deux moitiés.

Définition 28.2Règle d'inférence, dérivation

Une règle d'inférence se note

$\frac{pr e ˊ misses}{conclusion}$

et se lit « si l'on a établi les prémisses, on établit la conclusion ». Une dérivation — ou arbre de preuve — est un arbre dont chaque nœud est une instance de règle, et dont les feuilles sont des axiomes.

ImportantUn arbre de preuve est un type inductif, et rien de nouveau

La définition est celle du chapitre chap:induction :

$Γ , A ⊢ A (axiome) \frac{D _{1} \dots D _{k}}{Γ ⊢ C} (r e ˋ gle)$

On peut donc raisonner par induction sur la dérivation, exactement comme on raisonnait par induction sur une formule ou sur un arbre. C'est ce qui rendra la preuve de correction, plus bas, aussi courte.

Exemple 28.3Deux règles dérivées que le programme cite

$Modus ponens : p, p \to q ⊢ q$

$Syllogisme ba r ba r a : p \to q, q \to r ⊢ p \to r$

Le premier est l'élimination de l'implication ; le second se dérive en trois pas, et sa preuve est écrite plus loin.

28.3 Les règles de la déduction naturelle

Le programme demande « les règles pour $\land$ , $\lor$ , $\neg$ et $\to$ ». Chaque connecteur en a deux familles : comment le fabriquer (introduction) et comment s'en servir (élimination).

Définition 28.4Axiome, et les règles de

\land

$Γ , A ⊢ A ax \frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A \land B} \land_{i} \frac{Γ ⊢ A \land B}{Γ ⊢ A} \land_{e}^{g} \frac{Γ ⊢ A \land B}{Γ ⊢ B} \land_{e}^{d}$

Pour établir une conjonction, il faut établir les deux membres. Pour utiliser une conjonction, on en extrait le membre voulu.

Définition 28.5Les règles de

\to

$\frac{Γ , A ⊢ B}{Γ ⊢ A \to B} \to_{i} \frac{Γ ⊢ A \to B Γ ⊢ A}{Γ ⊢ B} \to_{e}$

ImportantLa règle

\to_{i}

est la plus importante du chapitre

Elle formalise le geste que tout mathématicien fait sans y penser : pour démontrer « si $A$ alors $B$ », on suppose $A$ et l'on démontre $B$ .

Lue de bas en haut, elle déplace $A$ de la droite du $⊢$ vers la gauche : $A$ cesse d'être un but et devient une hypothèse. C'est une décharge d'hypothèse, et c'est ce qui distingue la déduction naturelle d'un simple calcul de propagation.

Définition 28.6Les règles de

\lor

$\frac{Γ ⊢ A}{Γ ⊢ A \lor B} \lor_{i}^{g} \frac{Γ ⊢ B}{Γ ⊢ A \lor B} \lor_{i}^{d} \frac{Γ ⊢ A \lor B Γ , A ⊢ C Γ , B ⊢ C}{Γ ⊢ C} \lor_{e}$

L'élimination est le raisonnement par cas : si l'on sait $A \lor B$ et qu'on sait conclure $C$ dans chacune des deux hypothèses, alors $C$ est établi.

Définition 28.7Les règles de

\neg

En posant $\neg A$ comme $A \to ⊥$ :

$\frac{Γ , A ⊢ ⊥}{Γ ⊢ \neg A} \neg_{i} \frac{Γ ⊢ \neg A Γ ⊢ A}{Γ ⊢ ⊥} \neg_{e} \frac{Γ ⊢ ⊥}{Γ ⊢ C} ⊥_{e}$

$\neg_{i}$ est le raisonnement par l'absurde : on suppose $A$ , on aboutit à une contradiction, on conclut $\neg A$ . Et $⊥_{e}$ dit qu'une contradiction permet de tout conclure.

28.4 Écrire une petite preuve

Exemple 28.8Le syllogisme barbara

Montrons $p \to q, q \to r ⊢ p \to r$ . Posons $Γ = {p \to q, q \to r}$ .

$\frac{\frac{Γ , p ⊢ q \to r ax \frac{Γ , p ⊢ p \to q ax Γ , p ⊢ p ax}{Γ , p ⊢ q} \to _{e}}{Γ , p ⊢ r} \to _{e}}{Γ ⊢ p \to r} \to_{i}$

Comment on l'a trouvée : de bas en haut. Le but est $p \to r$ , donc $\to_{i}$ : on suppose $p$ et l'on vise $r$ . Pour obtenir $r$ , la seule hypothèse qui le produit est $q \to r$ , donc $\to_{e}$ : il reste à obtenir $q$ . Et $q$ s'obtient de $p \to q$ et de $p$ , tous deux dans le contexte.

Trois nœuds, quelle que soit la complexité des propositions $p$ , $q$ , $r$ — là où une table de vérité en aurait huit lignes, et $2^{n}$ si les lettres étaient des formules à $n$ variables.

Exemple 28.9L'exemple que le programme donne :

⊢ (p \to q) \to \neg (p \land \neg q)

$\frac{\frac{\frac{Δ ⊢ \neg q ax \frac{Δ ⊢ p \to q ax Δ ⊢ p ax}{Δ ⊢ q} \to _{e}}{Δ ⊢ ⊥} \neg _{e}}{p \to q ⊢ \neg ( p \land \neg q )} \neg _{i}}{⊢ ( p \to q ) \to \neg ( p \land \neg q )} \to_{i}$

où $Δ = {p \to q, p \land \neg q}$ , et où les séquents $Δ ⊢ p$ et $Δ ⊢ \neg q$ s'obtiennent en réalité de $Δ ⊢ p \land \neg q$ par $\land_{e}^{g}$ et $\land_{e}^{d}$ — deux pas qu'on abrège ici pour ne pas alourdir l'arbre.

Méthode : La stratégie : lire l'arbre de bas en haut

Regarder le but, à droite du $⊢$ . Sa forme désigne la règle d'introduction à employer : $\to$ appelle $\to_{i}$ , $\land$ appelle $\land_{i}$ , $\neg$ appelle $\neg_{i}$ .
Quand le but est atomique — une variable, ou $⊥$ — c'est qu'il faut éliminer : chercher dans le contexte une hypothèse qui le produise.
S'arrêter dès qu'un séquent a son but dans son contexte : c'est un axiome.

Cette montée est déterministe presque partout, ce qui explique que les preuves demandées soient courtes.

28.5 Correction

◆Théorème 28.10Correction de la déduction naturelle

Si $Γ ⊢ C$ , alors $Γ ⊨ C$ .

Démonstration (Par induction sur la dérivation)

On montre que chaque règle préserve la propriété « tout modèle du contexte est modèle du but ».

Axiome. Si $A \in Γ$ , tout modèle de $Γ$ satisfait $A$ . Immédiat.

$\land_{i}$ . Par hypothèse d'induction, tout modèle $v$ de $Γ$ satisfait $A$ et satisfait $B$ . La table de $\land$ donne alors $[[A \land B]]_{v} = V$ .

$\to_{i}$ . Soit $v$ un modèle de $Γ$ . Si $[[A]]_{v} = F$ , alors $[[A \to B]]_{v} = V$ par la table de $\to$ . Si $[[A]]_{v} = V$ , alors $v$ est un modèle de $Γ \cup {A}$ , donc de $B$ par hypothèse d'induction, donc $[[A \to B]]_{v} = V$ . Dans les deux cas la conclusion tient.

$\to_{e}$ . Soit $v$ modèle de $Γ$ . Par hypothèse d'induction, $[[A \to B]]_{v} = V$ et $[[A]]_{v} = V$ ; la table de $\to$ impose $[[B]]_{v} = V$ .

Les autres règles se traitent de même.

ImportantCe que la correction garantit, et ce qu'elle ne garantit pas

La correction dit : on ne peut pas démontrer de fausseté. C'est la moitié qui compte pour un utilisateur — un système incorrect serait inutilisable.

La moitié réciproque, la complétude — si $Γ ⊨ C$ alors $Γ ⊢ C$ —, est vraie aussi, mais elle est hors programme. On peut donc démontrer, dans ce système, toutes les conséquences logiques ; ce n'est pas à savoir, et surtout pas à démontrer.

iRemarqueLa contraposée de la correction, et son usage

Si $Γ \neq ⊨ C$ — s'il existe une valuation qui satisfait $Γ$ sans satisfaire $C$ — alors aucune dérivation de $C$ n'existe. Une seule ligne de table de vérité suffit donc à prouver qu'on cherche une preuve en vain, ce qui évite de longues recherches inutiles. Les deux outils ne s'opposent pas : la table réfute, la preuve établit.

28.6 Les quantificateurs

Le programme demande les règles « pour les quantificateurs universels et existentiels », et précise : « on motive ces règles par une approche sémantique intuitive ».

Définition 28.11Introduction et élimination de

\forall

$\frac{Γ ⊢ A ( x )}{Γ ⊢ \forall x A ( x )} \forall_{i} \frac{Γ ⊢ \forall x A ( x )}{Γ ⊢ A ( t )} \forall_{e}$

$\forall_{i}$ n'est légitime que si $x$ n'est libre dans aucune hypothèse de $Γ$ : c'est le « soit $x$ quelconque » des mathématiques, et la condition dit exactement que $x$ est arbitraire. $\forall_{e}$ est la spécialisation : ce qui vaut pour tous vaut pour $t$ .

Définition 28.12Introduction et élimination de

\exists

$\frac{Γ ⊢ A ( t )}{Γ ⊢ \exists x A ( x )} \exists_{i} \frac{Γ ⊢ \exists x A ( x ) Γ , A ( x ) ⊢ C}{Γ ⊢ C} \exists_{e}$

$\exists_{i}$ : exhiber un témoin suffit. $\exists_{e}$ : « soit $x$ un tel objet » — et $x$ ne doit être libre ni dans $Γ$ ni dans $C$ , faute de quoi on lui prêterait des propriétés qu'il n'a pas.

AttentionLes conditions de bord ne sont pas des formalités

Sans la condition sur $\forall_{i}$ , on démontrerait n'importe quoi. De $P (x) ⊢ P (x)$ on tirerait $P (x) ⊢ \forall y P (y)$ : « puisque cet objet-ci a la propriété, tous l'ont ». La condition l'interdit, car $x$ est libre dans l'hypothèse.

C'est exactement le piège des variables libres et liées du chapitre chap:logique, et c'est la même erreur qu'un programmeur commet en capturant une variable qu'il croyait locale.

28.7 Ce qu'il faut retenir

ImportantDéduction naturelle : cinq points

Un séquent $Γ ⊢ C$ affirme la démontrabilité, là où $Γ ⊨ C$ affirme la vérité. Syntaxe contre sémantique, une dernière fois.
Une dérivation est un arbre — un type inductif —, donc on y raisonne par induction.
Chaque connecteur a ses règles d'introduction (comment le fabriquer) et d'élimination (comment s'en servir).
$\to_{i}$ formalise « supposons $A$ , montrons $B$ » ; $\lor_{e}$ est le raisonnement par cas ; $\neg_{i}$ est le raisonnement par l'absurde. Ce ne sont pas des inventions : ce sont les gestes ordinaires des mathématiques, écrits.
La correction — on ne démontre que du vrai — se prouve par induction, règle par règle. La complétude est hors programme.

Et le gain qui justifie tout le chapitre : une preuve de trois nœuds remplace une table de $2^{n}$ lignes, et elle ressemble à ce qu'on écrit vraiment.

Continuer sur Adloun : animation, QCM, fiches, exercices