Déduction naturelle
Cours · informatique (MP2I/MPI), chapitre 28 · MP2I et MPI · le début du chapitre, la suite sur Adloun
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.
« 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 à variables a lignes de table. À , il y a plus de lignes que de secondes depuis le Big Bang. Une preuve, elle, peut tenir en dix lignes quelle que soit .
- 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.
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
Un séquent s'écrit
et se lit : « des hypothèses , on déduit ». La partie gauche est le contexte, souvent noté .
C'est la distinction syntaxe/sémantique du chapitre chap:logique, à son point le plus net.
| Nature | sémantique | syntaxique |
| Ce que cela dit | tout modèle de l'est de | il existe une dérivation de |
| Comment on l'établit | en examinant les valuations | en construisant un arbre |
| Coût | 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.
Une règle d'inférence se note
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.
Exercices du chapitre
- Une hypothèse qui ne sert pas corrigé
- Le raisonnement par cas corrigé
- La contraposée corrigé
- Réfuter en une ligne corrigé
- Trouver la faute corrigé
- Les conditions de bord des quantificateurs corrigé