Théorème de complétude de Gödel

Le théorème de complétude de la logique du premier ordre a été démontré pour la première fois par Kurt Gödel en 1929 dans sa thèse de doctorat, sur la complétude du calcul logique[3]. Leon Henkin a ensuite simplifié la démonstration dans sa thèse The Completeness of Formal Systems (la complétude des systèmes formels) publiée en 1949[4]. La preuve de Henkin a ensuite été simplifiée à son tour par Gisbert Hasenjaeger en 1953[5].

Le théorème de complétude est un méta-théorème[6] qui relie deux concepts : celui de conséquence sémantique et de conséquence syntaxique dans un système de déduction logique.

Un système de déduction pour le calcul des prédicats étant choisi, on montre que si une formule p est déductible, avec les règles de ce système à partir d'un ensemble T de formules (T⊢p), alors p est une conséquence sémantique de T, c’est-à-dire conséquence logique au sens de la théorie des modèles, voir ci-dessus (on note, pour distinguer de la notion précédente, T⊨p).

La preuve se fait par récurrence sur la taille des preuves, taille que l'on définit pour chaque système de déduction. Il s'agit alors de vérifier que chaque axiome logique est valide, et que chaque règle conserve la validité. La preuve est triviale, mais fastidieuse à rédiger entièrement.

Précisons un peu le cas de la déduction naturelle : il est plus commode d'utiliser une formulation de celle-ci en termes de séquents (ayant un nombre fini de prémisses et une conclusion).

Il faudrait manipuler des formules avec variables libres. Pour simplifier (l'idée est la même) faisons comme si nous étions en calcul propositionnel, c’est-à-dire que toutes les formules sont closes, il n'y a pas de quantificateurs. Un séquent est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion.

Un séquent est prouvable s'il est ou bien un axiome, ou bien déduit des axiomes par un nombre fini d'applications des règles de la déduction naturelle. Les axiomes sont ici tous les séquents de la forme p⊢p où p est une formule du calcul des prédicats. Comme on a de manière évidente p⊨p, les axiomes sont valides. On peut alors montrer, à partir de la définition de la vérité des formules complexes (voir théorie des modèles), qu'en partant de séquents valides, on ne peut déduire que des séquents valides si on applique une des règles de la déduction naturelle des séquents. On montre alors par induction sur la structure des preuves (essentiellement, c'est une récurrence sur la hauteur des preuves en tant qu'arbre) que tous les séquents prouvables sont valides.

Par exemple, supposons que l'on ait prouvé T⊢p∧q par introduction du connecteur logique ∧ (et). Cela signifie qu'auparavant, on a prouvé T⊢p et T⊢q. Par induction, on a T⊨p et T⊨q. Dans tout modèle rendant les formules de T vraies, p est vrai et q est vraie. Donc p∧q est vraie, et on a bien T⊨p∧q.

En appliquant la même vérification à tous les séquents, on prouve que, si T⊢p, alors T⊨p.

Pour en déduire que les formules prouvables (⊢p) sont des lois logiques (⊨p). Il suffit de prendre T vide.

Dans cette section, nous donnons les idées principales de la démonstration du théorème de complétude du premier ordre par Leon Henkin[7]. Nous démontrons la reformulation suivante du théorème de complétude :

La démonstration comprend deux étapes :

1. Nous ajoutons des formules à T afin que T soit complète (toute formule ou sa négation est dans T) et T est dite de Henkin, c'est-à-dire que si T contient une formule de la forme ${\displaystyle \exists x\psi (x)}$ alors T doit aussi contenir une formule ${\displaystyle \psi (c)}$ où c est une constante fraîche ;
2. Nous construisons un modèle "syntaxique" où les éléments du domaine sont les termes.

Nous allons prouver le théorème de complétude sous la forme suivante.

Si une formule est cohérente alors elle est satisfaisable. Si p⊬⊥ alors ⊭¬p.

En fait nous prouverons une version renforcée de ce théorème.

Si un ensemble d'axiomes est cohérent alors il est satisfaisable.

Un ensemble d'axiomes est cohérent lorsqu'aucune contradiction n'est prouvable à partir d'un nombre quelconque, fini, de ces axiomes. Il est satisfaisable lorsqu'il y a un modèle dans lequel les axiomes sont tous vrais. Cette version renforcée du théorème est utile en particulier pour énoncer le paradoxe de Skolem, parce qu’elle permet d’appliquer le théorème de complétude à des systèmes infinis d’axiomes.

Commençons par montrer comment remplacer un système d’axiomes du calcul des prédicats par un système équivalent d’axiomes du calcul des propositions. Pour cela, on commence par mettre chaque axiome sous une forme prénexe.

Une formule du calcul des prédicats est toujours équivalente à une formule mise sous forme prénexe, c’est-à-dire une formule dans laquelle tous les quantificateurs universels et existentiels sont placés au début et non à l'intérieur des sous-formules. On peut toujours prouver qu'une formule est équivalente à une formule prénexe avec les règles de déduction suivante :

• de (∃x p)∧q déduire ∃x(p∧q), pourvu que q ne contienne pas x comme variable libre. (Si elle la contient, il suffit de substituer à x dans ∃x p une autre variable qui n'apparaît pas dans q).
• de (∃x p)∨q déduire ∃x(p∨q), pourvu également que q ne contienne pas x comme variable libre.
• deux autres règles semblables pour le quantificateur universel ∀.
• de ¬(∃x p) déduire ∀x(¬p).
• de ¬(∀x p) déduire ∃x(¬p).

Toutes ces règles sont des règles dérivées dans le système de déduction naturelle et elles font toutes passer d'une prémisse à une conclusion équivalente. Par itération elles fournissent une formule prénexe équivalente à la formule initiale.

De la forme prénexe d'un axiome, on passe à sa forme de Skolem en introduisant de nouveaux opérateurs fondamentaux, autant qu’il en faut pour faire disparaître tous les quantificateurs existentiels dans les axiomes. Par exemple, l’axiome prénexe ∀x ∃y x+y=0 est remplacé par ∀x x+(–x)=0 où – est un nouvel opérateur unaire. Pour un axiome de la forme ∀x ∀y ∃z P(x,y,z), on introduit un opérateur binaire, ✲ par exemple, et on prend pour axiome ∀x ∀y P(x,y,x✲y).

On construit alors un univers, un domaine des êtres nommés. Les noms des objets de base sont ceux qui sont mentionnés dans les axiomes. S’il n’y en a pas, on en introduit un, qu’on peut appeler comme on veut, 0 par exemple.

L’ensemble des noms d’objet est celui obtenu par induction à partir des noms des objets de base et des noms de tous les opérateurs mentionnés dans les axiomes d’origine ou introduits par la méthode ci-dessus exposée. L’univers U est l’ensemble de tous les êtres ainsi nommés.

Chaque forme de Skolem d'un axiome peut être conçue comme un schéma d’axiomes à l'intérieur du calcul des propositions. On supprime tous les quantificateurs universels et on remplace toutes les variables alors libres par des noms d’objet. À chaque axiome de départ on associe ainsi un ensemble infini de formules du calcul des propositions. La réunion de toutes ces formules associées à tous les axiomes de départ, est le nouveau système d’axiomes, non quantifiés, équivalent au système d’origine.

Montrons maintenant que si un sous-ensemble fini du système d'axiomes non quantifiés est incohérent alors le système d'axiomes d'origine est lui aussi incohérent. Soit C une conjonction incohérente d'axiomes non quantifiés. Soit C' la formule obtenue à partir de C en remplaçant toutes ses constantes par des variables distinctes, de telle façon que C ne contienne plus d'opérateurs d'objet, et en quantifiant existentiellement sur toutes ces variables. Comme C est incohérente, C' l'est aussi. Mais C' peut être prouvée à partir d'un nombre fini des axiomes d'origine, qui sont donc eux aussi incohérents.

Si un système d'axiomes est cohérent tous les sous-ensembles finis du système d'axiomes non quantifiés sont également cohérents. D'après le théorème de complétude du calcul des propositions, ils sont donc tous satisfaisables. D'après le théorème de compacité, le système - infini - d'axiomes non quantifiés est lui aussi satisfaisable. Comme un modèle du système d'axiomes non quantifiés est également un modèle du système d'origine, on a prouvé l'existence d'un modèle pour tout système cohérent d'axiomes.

L'ensemble de noms à partir duquel un modèle est construit dans la preuve ci-dessus est dénombrable. On a donc prouvé également le théorème de Löwenheim-Skolem (prouvé en 1915 par Leopold Löwenheim et complété ensuite pour les systèmes infinis d'axiomes par Thoralf Skolem).

Si un système d'axiomes fini ou infini dénombrable a un modèle alors il a un modèle dénombrable.

On voit que la preuve repose sur le fait que dans un langage dénombrable (langage au sens large : les formules du langage de la théorie en font partie) on ne peut traiter que d'une collection dénombrable d'objets.

Appliqué à la théorie des ensembles, ce théorème semble paradoxal. La théorie des ensembles de Zermelo et ses extensions comme la théorie ZFC sont développées dans un langage dénombrable, qui utilise un ensemble infini dénombrable d'axiomes. Donc cette théorie et ces extensions ont un modèle dénombrable.

En utilisant l'axiome de l'infini et l'axiome de l'ensemble des parties, on montre l'existence de l'ensemble P(ℕ) de tous les ensembles d'entiers. Cantor a montré, en utilisant, le raisonnement diagonal, que cet ensemble n'est pas dénombrable (les autres axiomes de la théorie des ensembles de Zermelo sont utiles pour formaliser le raisonnement).

Le paradoxe n'est qu'apparent ; il disparait dès que l'on pense que le modèle dénombrable dont on a montré l'existence ne s'identifie pas avec l'univers dans lequel on a travaillé pour montrer celle-ci. En particulier « dénombrable » ne signifie plus la même chose à l'intérieur de ce modèle dénombrable.

En effet on sait que dans un modèle (ou univers) de la théorie des ensembles, dont les objets sont des ensembles, il existe des collections d'objets (des ensembles au sens intuitif), que l'on peut éventuellement définir par une formule, par exemple les objets qui ne s'appartiennent pas à eux-mêmes (voir paradoxe de Russell), mais qui ne sont pas des ensembles : on ne peut trouver d'objet du modèle auquel appartiennent les objets d'une de ces collections (et seulement ceux-ci). Or dire qu'un ensemble est dénombrable, c'est dire qu'il existe une fonction, c’est-à-dire un ensemble de couples, qui est une bijection de ${\displaystyle \mathbb {N} }$ dans cet ensemble. Dans un modèle dénombrable de la théorie des ensembles, on a une collection de couples qui établit une bijection entre l'ensemble ℕ du modèle et l'ensemble P(ℕ) du modèle. Mais cette collection n'est pas un ensemble, c’est-à-dire un objet du modèle dénombrable[8]. Dit de façon abrupte, du point de vue du modèle dénombrable, P(ℕ) n'est effectivement pas dénombrable.

On peut discuter de ce que veut dire « au sens intuitif » dans l'explication ci-dessus : c'est une commodité d'expression. Tout ceci se formalise dans une théorie des ensembles (plus forte que celle que l'on étudie). Dit sémantiquement, dans l'univers de la théorie des ensembles dans lequel on travaille, on a défini un modèle, un objet de cet univers, qui est un modèle dénombrable (au sens de cet univers) de la théorie de Zermelo, mais à l'intérieur duquel, au sens maintenant du modèle que l'on a construit, il existe des ensembles non dénombrables.

• Déduction naturelle
• Démonstration
• Théorème de complétude (calcul des propositions)
• Théorèmes d'incomplétude de Gödel
• Décidabilité

• Raymond Smullyan, First order logic 1968 (ISBN 0486683702)
• Kurt Gödel, Collected works, vol 1 (ISBN 0195039645)
• Alonzo Church, Introduction to mathematical logic 1956 (ISBN 0691029067)
• René David, Karim Nour, Christophe Raffali, Introduction à la logique, théorie de la démonstration 2001, Dunod, (ISBN 2100067966)