Démontrer au premier ordre : quatre règles, un théorème de Gödel et quelques vertiges
Bonne nouvelle : pour démontrer en calcul des prédicats, on garde tout ce qu’on a construit pour le calcul des propositions. Les séquents, les arbres de preuve, les règles d’introduction et d’élimination de chaque connecteur, l’absurdité classique : rien ne change. Il suffit d’ajouter une règle d’introduction et une règle d’élimination pour chacun des deux quantificateurs.
Dans ce qui suit, $\phi(t)$ désigne la formule $\phi(x)$ dans laquelle on a remplacé la variable libre $x$ par le terme $t$.
Les deux règles faciles
Les deux règles délicates
« Soit $x$ un nombre quelconque. Supposons $x=2$. Alors $x$ est pair. Comme $x$ était quelconque, tous les nombres sont pairs. »
L’erreur saute aux yeux en français, et la règle $\forall i$ la rend mécanique : on a prouvé $x=2\vdash\mathit{Pair}(x)$, mais la variable $x$ est libre dans l’hypothèse $x=2$. Elle n’était donc pas quelconque du tout, et la généralisation est interdite.
Socrate, enfin. Avec $H$ pour « homme », $M$ pour « mortel » et $s$ pour Socrate :
Échanger les quantificateurs. S'il existe quelqu'un que tout le monde aime, alors tout le monde aime quelqu'un :
Le $\forall i$ est permis car $x$ est liée dans l'hypothèse $\forall x\,R(x,y)$, et le $\exists e$ l'est car $y$ ne figure pas, libre, dans la conclusion. L'inverse est impossible à prouver, et c'est heureux : la figure sur l'ordre des quantificateurs montre une situation où tout le monde aime quelqu'un sans que personne ne soit aimé de tous.
Le calcul des prédicats a donc ses preuves (le symbole $\vdash$) et sa sémantique (le symbole $\models$, « vrai dans toutes les structures où les hypothèses sont vraies »). Coïncident-ils, comme en calcul des propositions ?
Théorème de complétude (Gödel, 1929) : pour tout ensemble d'énoncés $\Gamma$ et tout énoncé $\phi$,
$\Gamma\models\phi$ si et seulement si $\Gamma\vdash\phi$.
Tout ce qui est vrai dans toutes les structures se démontre, et rien d’autre. La question avait été posée en 1928 par David Hilbert et Wilhelm Ackermann dans leur manuel de logique. Kurt Gödel, 23 ans, y répond l’année suivante dans sa thèse de doctorat à Vienne.
La preuve qu’on enseigne aujourd’hui, due à Leon Henkin (1949), suit la même idée que la complétude des logiques modales : fabriquer une structure à partir de la syntaxe elle-même. Les objets du domaine sont les termes du langage, et, pour que chaque « il existe » ait de quoi se réaliser, on ajoute au langage une nouvelle constante, un témoin, pour chaque formule $\exists x,\phi(x)$.
Complétude et incomplétude ne se contredisent pas, malgré les noms et l’auteur commun. Le théorème de complétude (1929) dit que les règles de preuve attrapent toutes les conséquences logiques d’un ensemble d’axiomes. Les théorèmes d’incomplétude (1931) disent qu’un ensemble d’axiomes pour l’arithmétique ne décide jamais tous les énoncés : il en reste qui ne sont ni démontrables ni réfutables. Les deux se concilient très bien : un tel énoncé est vrai dans certaines structures qui satisfont les axiomes et faux dans d’autres, donc il n’est pas une conséquence logique des axiomes, et la complétude n’oblige pas à le démontrer.
Une preuve n’utilise qu’un nombre fini d’hypothèses. Grâce à la complétude, cette banalité devient un théorème surprenant sur les structures.
Théorème de compacité : si chaque partie finie d'un ensemble d'énoncés $\Gamma$ a une structure qui la rend vraie, alors $\Gamma$ tout entier en a une.
En effet, si $\Gamma$ n’avait aucune structure, on pourrait en déduire une contradiction (complétude), et cette preuve n’utiliserait qu’une partie finie de $\Gamma$, qui serait donc déjà contradictoire.
Premier vertige : la finitude est indicible. Supposons qu’un énoncé $\phi$ dise « le domaine est fini ». Ajoutons-lui les énoncés « il y a au moins $n$ objets », pour tous les $n$. Chaque partie finie de cette liste n’en mentionne qu’un nombre fini et a donc une structure (finie, assez grande). Par compacité, la liste entière a une structure, à la fois finie et plus grande que tout entier : c’est absurde. Aucune formule ne sait dire « fini ».
Second vertige : des entiers infiniment grands. Prenons tous les énoncés vrais sur les entiers, et ajoutons une nouvelle constante $c$ avec les axiomes $c>0$, $c>1$, $c>2$, et ainsi de suite. Chaque partie finie est vraie dans les entiers usuels (il suffit de choisir $c$ assez grand). Par compacité, il existe une structure qui vérifie tous les énoncés vrais de l’arithmétique et qui contient pourtant un « entier » $c$ plus grand que $0$, que $1$, que $2$… Aucun énoncé du premier ordre ne la distingue des entiers ordinaires.
Un modèle non standard de l'arithmétique : les entiers usuels, puis, au-delà de tous, des entiers infiniment grands (un tel entier $c$ a toujours un prédécesseur $c-1$ et un successeur $c+1$).
Thoralf Skolem construit de tels modèles non standard de l’arithmétique dès 1934. Vers 1960, Abraham Robinson applique la même idée aux nombres réels : la compacité fournit des réels infiniment petits, plus petits que $1/n$ pour tout $n$ et pourtant non nuls. Les infinitésimaux de Leibniz, que les mathématiciens du XIXe siècle avaient bannis comme incohérents, retrouvent ainsi une existence parfaitement rigoureuse. C’est l’analyse non standard.
Théorème de Löwenheim-Skolem : un ensemble d'énoncés écrits dans un langage dénombrable qui possède une structure infinie possède aussi une structure **dénombrable**.
Or la théorie des ensembles s’écrit au premier ordre, dans un langage qui ne contient qu’un symbole, $\in$. Elle démontre, avec l’argument diagonal de Cantor, qu’il existe des ensembles non dénombrables, comme l’ensemble des réels. Et pourtant, d’après Löwenheim-Skolem, elle possède un modèle dénombrable ! C’est le paradoxe de Skolem (1922).
Il n’y a pas de contradiction. Dans ce modèle, « l’ensemble des réels » n’a qu’une quantité dénombrable d’éléments vue de l’extérieur ; mais la bijection qui le prouverait n’appartient pas au modèle. Vu de l’intérieur, l’ensemble est bel et bien non dénombrable, puisqu’aucune bijection avec les entiers n’y existe. « Dénombrable » est une notion relative au monde dans lequel on se place. Skolem en concluait que la théorie des ensembles ne pouvait pas servir de fondement absolu aux mathématiques.
En calcul des propositions, on sait décider mécaniquement si une formule est une tautologie : il suffit de dresser sa table de vérité. En 1928, Hilbert pose la même question pour le calcul des prédicats : c’est le célèbre Entscheidungsproblem, le « problème de la décision ».
La réponse, négative, arrive en 1936, deux fois la même année. Alonzo Church avec le lambda-calcul, puis Alan Turing avec ses machines, montrent qu’aucun algorithme ne décide si un énoncé du premier ordre est universellement valide. Pour y parvenir, Turing a dû d’abord définir précisément ce qu’est un algorithme : l’informatique théorique est née de cette question de logique.
On peut seulement énumérer les preuves, l’une après l’autre. Si l’énoncé est valide, on finira par tomber sur sa preuve (la complétude le garantit). S’il ne l’est pas, la recherche peut durer éternellement sans qu’on puisse jamais savoir s’il faut continuer à chercher. On dit que la validité est semi-décidable.
| Calcul des propositions | Calcul des prédicats | |
|---|---|---|
| correct et complet | oui (Post, 1921) | oui (Gödel, 1929) |
| compact | oui | oui |
| décidable | oui, par les tables de vérité | non (Church, Turing, 1936), seulement semi-décidable |
Une théorie est un ensemble d’énoncés qu’on prend pour axiomes. La plus célèbre est l’arithmétique de Peano, notée $\text{PA}$. Son langage contient la constante $0$, la fonction successeur ($x\mapsto x+1$), l’addition et la multiplication. Ses axiomes disent par exemple que $0$ n’est le successeur de personne, et comment calculer $x+(y+1)$ ou $x\times(y+1)$.
La récurrence pose le problème annoncé au début. Faute de pouvoir dire « pour toute propriété », on l’écrit sous forme de schéma : un axiome distinct pour chaque formule $\phi(x)$,
$$\big(\phi(0)\land\forall x,(\phi(x)\rightarrow\phi(x+1))\big)\rightarrow\forall x,\phi(x).$$
Les formules sont dénombrables, alors que les propriétés des entiers (les ensembles d’entiers) ne le sont pas. Le schéma laisse donc échapper l’immense majorité des propriétés, et c’est par cette brèche que s’engouffrent les modèles non standard.
C’est dans ce cadre que se jouent les théorèmes d’incomplétude de Gödel : $\text{PA}$, comme toute théorie raisonnable qui la contient, laisse des énoncés vrais sans démonstration. Comme l’arithmétique peut parler de ses propres preuves, on peut lire ces théorèmes avec une boîte de logique modale. C’est l’objet de la rubrique suivante.