Correction et complétude

Deux questions sur le système du cours

L’unité sur la déduction a fixé le système du cours : les schémas d’axiomes A1, A2 et A3 de Łukasiewicz et deux règles, le modus ponens (MP) et le remplacement de la double négation (RDN), que la leçon sur les quatre techniques de déduction a ajouté après avoir démontré la double négation. Une déduction à partir d’un ensemble $\Gamma$ est une suite finie de formules dans laquelle chacune est un axiome, un élément de $\Gamma$, le résultat du modus ponens appliqué à deux formules antérieures ou le résultat de RDN appliqué à une formule antérieure ; $\Gamma \vdash \varphi$ signifie qu’il existe une déduction à partir de $\Gamma$ dont la dernière formule est $\varphi$. L’unité sur la sémantique, de son côté, a défini dans la leçon sur la conséquence et l’équivalence sémantiques la relation $\Gamma \models \varphi$ : toute valuation qui satisfait toutes les formules de $\Gamma$ satisfait $\varphi$. Les deux relations s’écrivent selon le même schéma, un ensemble à gauche et une formule à droite ; or leur nature est opposée. La première est syntaxique et existentielle : elle affirme qu’il existe un objet fini, une déduction, que l’on peut vérifier symbole par symbole. La seconde est sémantique et universelle : elle affirme quelque chose de toutes les valuations, qui sont en nombre infini, et dont chacune donne une valeur à une infinité de variables.

Deux questions se posent donc au sujet du système. La première : ne déduit-il que ce qu’il doit ? On dit que le système est correct si, pour tout ensemble $\Gamma$ et toute formule $\varphi$, $\Gamma \vdash \varphi$ implique $\Gamma \models \varphi$ : ce qui se déduit de certaines prémisses est vrai sous toute valuation qui rend les prémisses vraies. La seconde : déduit-il tout ce qu’il doit ? On dit que le système est complet si $\Gamma \models \varphi$ implique $\Gamma \vdash \varphi$. La complétude admet trois degrés, selon les ensembles de prémisses qu’elle couvre :

• complétude faible : si $\models \varphi$, alors $\vdash \varphi$ ; toute tautologie est un théorème ;
• complétude pour les ensembles finis : si $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi$, alors $\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ ;
• complétude forte : si $\Gamma \models \varphi$, alors $\Gamma \vdash \varphi$, pour un ensemble $\Gamma$ quelconque, même infini.

Cette leçon démontre la correction et les deux premiers degrés de la complétude. Le troisième est démontré dans la leçon sur le théorème de compacité, et la raison de ce partage sera expliquée à la fin de la leçon.

Ce qu’il ne faut pas dire

En espagnol, on appelle parfois la correction « solvencia », calque de l’anglais soundness ; le terme espagnol est « corrección », et c’est celui que le cours emploie en espagnol. Il ne faut pas non plus la définir comme la propriété du système « d’inférer une expression à partir d’un ensemble d’expressions », qui est la déductibilité elle-même et non une propriété du système. Les erreurs de fond, cependant, sont deux autres.

La première consiste à affirmer que la correction et la complétude « peuvent s’inférer l’une de l’autre ». Ce sont des propriétés indépendantes : le système de Łukasiewicz, sans la règle RDN, est correct (la démonstration de cette leçon le prouve, en supprimant un cas) et n’est pas complet (la leçon sur les systèmes déductifs formels a exhibé une tautologie qu’il ne déduit pas) ; et un système qui adopterait toutes les formules comme axiomes serait complet sans être correct. Le problème résolu 2 examine les deux exemples.

La seconde erreur est plus grave, parce qu’elle présente comme démonstration de la complétude un argument circulaire. Elle dit, en substance : si $\varphi \nvdash \psi$, alors, par le théorème de déduction, $\nvdash (\varphi \rightarrow \psi)$ ; « par la correction », $\not\models (\varphi \rightarrow \psi)$ ; et par le théorème de déduction sémantique, $\varphi \not\models \psi$. Or la correction dit que ce qui est déductible est valide, et sa contraposée, que ce qui n’est pas valide n’est pas déductible :

Le pas de l’argument va dans l’autre sens, de $\nvdash \chi$ à $\not\models \chi$, qui est la contraposée de $\models \chi \Rightarrow \vdash \chi$, c’est-à-dire de la complétude faible. S’il en est ainsi, l’argument suppose ce qu’il prétend démontrer. Il s’ensuit que la complétude ne « s’infère pas de façon simple » : c’est le résultat le plus profond du cours, et sa démonstration occupe la plus grande partie de cette leçon. Enfin, il est inexact de résumer la complétude en disant que « toutes les expressions vraies ont une démonstration » ; ce qui a une démonstration, c’est ce qui est valide, vrai sous toute valuation, non ce qui est vrai sous l’une d’elles : la variable $v_{1}$ est vraie sous beaucoup de valuations, et ce n’est pas un théorème.