Théorème de complétude de Gödel
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

Le théorème de complétude du calcul des prédicats du premier ordre a été prouvé par Kurt Gödel (1929, thèse de doctorat, Sur la complétude du calcul logique). Il affirme que le calcul des prédicats est complet au sens où on connaît des listes finies et complètes de tous ses principes. Autrement dit toute démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment...) mathématique peut en principe se formaliser en calcul des prédicats (Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des...).

Nous allons donner plusieurs définitions équivalentes de cette notion de complétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en un sens qu'il faut préciser...).

Diverses formulations équivalentes du théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit à partir...) de complétude

On peut donner un nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) fini d’axiomes, de schémas d’axiomes ou de règles de déduction tel que toutes les preuves logiquement valides formulées avec la grammaire du calcul des prédicats du premier ordre soient obtenues à partir de ces principes.

La notion de validité logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois...) d’une preuve est précisée par la théorie des modèles (La théorie des modèles est une théorie de la vérité mathématique. Elle consiste essentiellement à dire qu’une théorie est mathématiquement valide si on peut définir un univers dans lequel elle est vraie.). Une règle de déduction est valide lorsque tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) modèle de ses prémisses est aussi un modèle de sa conclusion. Un axiome logique (La méthode axiomatique permet de définir l'ensemble des lois logiques du premier ordre à partir d'axiomes logiques et de règles de déduction de telle...) 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 de déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner) 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 (La formulation est une activité industrielle consistant à fabriquer des produits homogènes, stables et possédant des propriétés...) des principes logiques, celle des Principia Mathematica de Whitehead et Russell.

Pour cela, donnons quelques définitions :

  • celles relatives à l'utilisation de modèles (du premier ordre) : satisfaisabilité et falsifiabilité, loi logique et contradiction (Une contradiction existe lorsque deux affirmations, idées, ou actions s'excluent mutuellement.) 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 \vDash 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 \vDash 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 \vDash \lnot p. Dire que p est satisfaisable, c'est dire que p n'est pas une contradiction logique, ce qu'on note \not{\vDash} \lnot 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 (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une évolution...) 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 \vdash p. Si T est un ensemble (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un tout », comme...) 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 \vdash q ou \vdash_T q . Les systèmes de déduction L pour des formules qui utilisent l'implication \to vérifient souvent p \vdash q si et seulement si \vdash p\to q (c'est le cas de la déduction naturelle, des système à 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 \vdash q dans L.

Notons \bot la contradiction, si elle ne fait pas partie du lanage on peut la définir par q \land \lnot q pour une formule close arbitraire q. Un ensemble de formules T est cohérent dans L lorsque 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 \not{\vdash} \bot. 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 \vdash \bot.

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 \vdash p alors \vDash 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 (En 1935 Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au plus près à la manière dont les mathématiciens raisonnent. Il a...).

Le théorème de complétude se préoccupe de la réciproque (La réciproque est une relation d'implication.). Cela signifie que le système de déduction L se doit d'être suffisamment complet (d'où le nom du théorème) de façon à pouvoir prouver toute loi logique, i.e. 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 infi 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 \vDash q alors p \vdash q.
  • Pour toute formule p, si p est une loi logique alors p est prouvable. Si \vDash p alors \vdash p.
  • Pour toute formule p, si p est une contradiction logique alors (non p) est prouvable. Si \vDash \lnot p, alors \vdash \lnot p.
  • Pour toute formule p, si p est une contradiction logique alors p est incohérente dans L. Si \vDash \lnot p, alors p \vdash \bot.
  • Pour toute formule p, si p est cohérente dans L alors p est satisfaisable. Si p \not{\vdash} \bot alors \not{\vDash} \lnot 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 (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée sur...) de l'indécidabilité (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.), 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 (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en...) 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 c est déductible, avec les règles de ce système à partir d'un ensemble de formules h (h \vdash c), 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, h \vDash c).

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 (Un axiome (du grec ancien αξιωμα/axioma, « considéré comme digne, convenable, évident en soi ») désigne une vérité indémontrable qui doit...) 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 \vdash p où p est une formule du calcul des prédicats. Comme on a de manière évidente p \vDash p, les axiomes sont valides. On peut alors montrer, à partir de la définition (Une définition est un discours qui dit ce qu'est une chose ou ce que signifie un nom. D'où la division entre les définitions réelles et les définitions nominales.) 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 (La hauteur a plusieurs significations suivant le domaine abordé.) des preuves en tant qu'arbre) que tous les séquents prouvables sont valides.

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

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

Pour en déduire que les formules prouvables (\vdash p) sont des lois logiques (\vDash p). Il suffit de prendre h vide (Le vide est ordinairement défini comme l'absence de matière dans une zone spatiale.).

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 \not{\vdash} \bot, alors \not{\vDash} \lnot 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 (Un paradoxe est une proposition qui contient ou semble contenir une contradiction logique, ou un raisonnement qui, bien que sans faille apparente, aboutit à une...) 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 (Le calcul des propositions ou calcul propositionnel, dont le fondateur fut le logicien allemand Frege, version moderne de la logique stoïcienne, est une théorie logique...). 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 (\exists x \;p) \land q déduire \exists x \;(p \land q), pourvu que q ne contienne pas x comme variable (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. ...) libre. (Si elle la contient, il suffit de substituer à x dans \exists x \;p une autre variable qui n'apparaît pas dans q).
  • de (\exists x \;p) \lor q déduire \exists x \;(p \lor q), pourvu également que q ne contienne pas x comme variable libre.
  • deux autres règles semblables pour le quantificateur universel \forall x.
  • de \lnot(\exists x \;p) déduire \forall x \;(\lnot p).
  • de \lnot(\forall x \;p) déduire \exists x \;(\lnot 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 (Le genre Passer a été créé par le zoologiste français Mathurin Jacques Brisson (1723-1806) en 1760.) 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 \forall x \; \exists y \; x+y = 0 est remplacé par \forall x \; x+(-x) = 0 est un nouvel opérateur (Le mot opérateur est employé dans les domaines :) unaire. Pour un axiome de la forme \forall x \; \forall y \; \exists z \; P(x,y,z), on introduit un opérateur binaire, * par exemple, et on prend pour axiome \forall x \; \forall y \; P(x,y,x*y)

On construit alors un univers (L'Univers est l'ensemble de tout ce qui existe et les lois qui le régissent.), 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 (En mathématiques, un ensemble est infini s'il n'est pas fini, c'est-à-dire s'il contient un nombre infini d'éléments. En d'autres termes, si E est un ensemble infini alors  : Le cardinal de E n'est pas un entier naturel. On dit...) de formules du calcul des propositions. La réunion (La Réunion est une île française du sud-ouest de l'océan Indien située dans l'archipel des Mascareignes à environ 700...) 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 (En mathématiques, un ensemble A est un sous-ensemble ou une partie d’un ensemble B, ou encore B est sur-ensemble de A, si tout élément du sous-ensemble A est aussi élément du sur-ensemble B. Il peut par contre y...) 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 (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise, et qui peut être désigné par une étiquette verbale....), 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é (Il s'agit d'énoncer et de prouver le théorème de compacité du calcul des propositions. Ce théorème a un rôle très important pour la logique du premier ordre,...), le système - infini (Le mot « infini » (-e, -s ; du latin finitus, « limité »), est un adjectif servant à qualifier quelque chose qui n'a pas de limite en nombre ou en taille.) - 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 (Le théorème de Löwenheim-Skolem fait partie de la théorie des modèles. Sa simplicité et sa puissance en font un théorème majeur — avec le théorème de compacité.) (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 (La théorie des ensembles est une branche des mathématiques créée initialement par le mathématicien allemand Georg Cantor à la fin du XIXe siècle.), ce théorème semble paradoxal. La théorie des ensembles de Zermelo et ses extensions comme la théorie ZFC (En mathématiques, l'abréviation ZF désigne la théorie de Zermelo-Fraenkel, ZFC quand elle comprend l'axiome du choix, théorie axiomatique des ensembles la plus couramment utilisée en mathématiques contemporaines. Bien que la...) 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 \mathcal P(\N) l'ensemble de tous les ensemble 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 (Une fonction f: X → Y est dite bijective ou est une bijection si pour tout y dans l’ensemble d'arrivée Y il existe un et un seul x dans l’ensemble de définition X tel que...) de \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 \N du modèle et l'ensemble \mathcal P(\N) du modèle. Mais cette collection n'est pas un ensemble, c’est-à-dire un objet du modèle dénombrable[1]. Dit de façon abrupte, du point (Graphie) de vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) du modèle dénombrable, \mathcal P(\N) 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

  1. Remarquons que cette collection, contrairement à la collection des ensembles qui ne s'appartiennent pas à eux-mêmes, n'est même pas une classe, c’est-à-dire définie par une formule, puisque, par compréhension, ce serait un ensemble.
Page générée en 1.452 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique