Théorème de complétude de Gödel - Définition

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 c est déductible, avec les règles de ce système à partir d'un ensemble de formules h ( ), alors c est une conséquence sémantique de h, 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, ).

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 où p est une formule du calcul des prédicats. Comme on a de manière évidente , 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é par introduction du connecteur logique (et). Cela signifie qu'auparavant, on a prouvé et . Par induction, on a et . Dans tout modèle rendant les formules de h vraies, p est vrai et q est vraie. Donc est vraie, et on a bien .

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

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

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 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 du modèle. Mais cette collection n'est pas un ensemble, c’est-à-dire un objet du modèle dénombrable. Dit de façon abrupte, du point de vue du modèle dénombrable, 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.