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

Le théorème de complétude du calcul des prédicats du premier ordre est un résultat fondamental en logique mathématique ; il a été démontré par Kurt Gödel (1929, thèse de doctorat, sur la complétude du calcul logique).

En termes intuitifs le théorème de complétude dresse un pont entre mathématiques informelles (exprimées dans le langage mathématique usuel) et mathématiques formelles (exprimées dans le système syntaxique du calcul des prédicats) en établissant que si on dispose d'une démonstration d'un énoncé alors on peut formaliser celle-ci ; la syntaxe est donc complète dans le sens où elle permet de représenter n'importe quelle démonstration informelle.

Plus précisément le théorème de complétude affirme que si un énoncé est conséquence sémantique d'une théorie, c'est-à-dire qu'il est vérifié dans tous les modèles de cette théorie, alors il est conséquence syntaxique de cette théorie : il existe une démonstration formelle dans la syntaxe du calcul des prédicats qui dérive cet énoncé à partir des axiomes de la théorie en utilisant les règles d'un système de déduction comme la déduction naturelle, le calcul des séquents ou un système à la Hilbert.

Diverses formulations équivalentes du théorème de complétude

Le théorème de complétude est un méta-théorème^[1] qui relie deux concepts : celui de déduction logique et celui de validité d'un énoncé.

Systèmes de déduction et validité

Le premier concept à définir est donc celui de déduction logique, il dit qu'on peut donner un nombre fini d’axiomes, de schémas d’axiomes ou de règles d'inférence pour décrire ou formaliser la partie purement logique de la déduction, autrement dit toutes les démonstrations qui sont décrites en des étapes élémentaires de raisonnement sont obtenues à partir de ces principes.

La validité logique d’un axiome, d'un schéma d'axiomes ou d'une règle d'inférence est garantie par des modèles. Ainsi, une règle de déduction est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion. Un axiome logique est valide lorsqu’il est vrai dans tous les modèles. Un schéma d’axiomes est un principe logique valide lorsque tous les axiomes produits par ce schéma sont des axiomes logiques valides. Un système de principes logiques est valide ou correct lorsque ses axiomes, ses schémas d’axiomes et ses règles de déduction sont valides. Une preuve est logiquement valide lorsqu’elle peut être formalisée dans le cadre d’un système logique valide.

Nous allons prouver que la liste des quinze règles^{[réf. souhaitée]} de déduction naturelle est un système complet des principes de la logique du premier ordre. Ce théorème est équivalent à celui de Gödel. Mais la preuve de Gödel est basée sur une autre formulation des principes logiques, celle des Principia Mathematica de Whitehead et Russell.

Quelques définitions

Pour cela, donnons quelques définitions :

• celles relatives à l'utilisation de modèles (du premier ordre) : satisfaisabilité et falsifiabilité, loi logique et contradiction logique, conséquence logique, prouvabilité :

Une formule du calcul des prédicats est satisfaisable ou possiblement vraie lorsqu’elle est vraie dans au moins un modèle. Elle est universellement valide, ou est une loi logique, lorsqu’elle est vraie dans tous les modèles. Si p est une loi logique, on note ⊨p. Si p et q sont deux formules du calcul des prédicats, on dira que q est une conséquence logique de p lorsque tout modèle de p est aussi un modèle de q, autrement dit, pour tout modèle m, si p est vrai dans m alors q est vrai dans m, ce qu'on note p⊨q. Une formule est falsifiable ou possiblement fausse lorsqu’elle est fausse dans au moins un modèle. Elle est absolument fausse, ou est une contradiction logique, lorsqu’elle est fausse dans tous les modèles. Sa négation est donc une loi logique. Si p est une contradiction logique, on a donc ⊨¬p. Dire que p est satisfaisable, c'est dire que p n'est pas une contradiction logique, ce qu'on note ⊭¬p ;

• celles relatives aux systèmes de déduction (pour le calcul des prédicats du premier ordre) : cohérence et incohérence, prouvabilité :

Si p est une formule du calcul des prédicats, p est prouvable dans un système de déduction pour la logique L, lorsqu’il existe une preuve de p dans L, au sens où les règles de déduction de L suffisent pour déduire p en un nombre fini d'étapes dans L, ce qu'on note ⊢p. Si T est un ensemble de formules du calcul des prédicats, p est prouvable à partir de T dans le système logique L, lorsqu’il existe une preuve de p à partir de certaines des formules de T (en nombre nécessairement fini) dans L, ce qu'on note T⊢q ou ⊢_T q. Les systèmes de déduction L pour des formules qui utilisent l'implication → vérifient souvent p⊢q si et seulement si ⊢p→q (c'est le cas de la déduction naturelle, des systèmes à la Hilbert, ou du calcul des séquents). Autrement dit, il est équivalent de prouver q à partir de p dans L, ou de prouver directement ⊢p→q dans L.

Notons ⊥ la contradiction, si elle ne fait pas partie du langage on peut la définir par q∧¬q pour une formule close arbitraire q. Un ensemble de formules T est cohérent dans L lorsqu'il existe une formule q qui n’est pas prouvable à partir de T dans L, ou de façon équivalente en logique classique, si la contradiction n'est pas prouvable à partir de T, ce qu'on note T⊬⊥. Un ensemble de formules T est incohérent ou contradictoire dans L lorsque toutes les formules sont prouvables à partir de T dans L, ou de façon équivalente en logique classique, si la contradiction est prouvable à partir de T, ce qu'on note T⊢⊥.

Un système de déduction correct se doit de ne pouvoir prouver, à partir de formules vraies, que des propositions vraies, en particulier, on attend que, si ⊢p alors ⊨p. Nous montrerons dans le paragraphe suivant que tel est le cas pour la déduction naturelle, ou un système équivalent, tel le calcul des séquents.

La complétude

Le théorème de complétude se préoccupe de la réciproque de la correction. Cela signifie que le système de déduction L se doit d'être suffisamment complet de façon à être capable de démontrer toute loi logique, c'est-à-dire toute formule vraie dans tout modèle. Le théorème de complétude peut être énoncé sous la forme suivante (exprimée pour une formule, une forme plus forte du théorème de complétude s'écrit pour un nombre éventuellement infini de formules) :

Il existe des systèmes de déduction logiques valides L qui satisfont aux conditions équivalentes suivantes :

• pour toutes formules p et q (du calcul des prédicats du premier ordre), si q est une conséquence logique de p alors q est prouvable à partir de p dans L. Si p⊨q alors p⊢q.
• Pour toute formule p, si p est une loi logique alors p est prouvable. Si ⊨p alors ⊢p.
• Pour toute formule p, si p est une contradiction logique alors (non p) est prouvable. Si ⊨¬p, alors ⊢¬p.
• Pour toute formule p, si p est une contradiction logique alors p est incohérente dans L. Si ⊨¬p, alors p⊢⊥.
• Pour toute formule p, si p est cohérente dans L alors p est satisfaisable. Si p⊬⊥ alors ⊭¬p.

On peut enfin remarquer qu'un ensemble défini par induction avec un nombre fini de principes (axiomes, schémas d'axiomes et règles de déduction) est énumérable. Autrement dit, toutes les théories axiomatiques usuelles sont des ensembles énumérables. Le théorème de complétude dit qu'il existe des théories axiomatiques complètes de la logique du premier ordre.

Il en résulte que l'ensemble des lois logiques est énumérable.

Cela permet de relier ce théorème de complétude à la théorie de l'indécidabilité, parce qu'on peut prouver que l'ensemble des lois logiques est indécidable. Autrement dit, l'ensemble des formules falsifiables n'est pas énumérable, ou, de façon équivalente, l'ensemble des formules satisfaisables n'est pas énumérable (voir également le théorème d'incomplétude et le théorème de Tarski).

La validité du calcul des prédicats du premier ordre

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.

L'existence d'un modèle sous l'hypothèse de cohérence

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.

Le théorème de Löwenheim et le paradoxe de Skolem

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 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^[2]. 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.

Notes

Voir aussi

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

Bibliographie

• 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)

• Portail de la logique
• Portail des mathématiques