Théorème de complétude de Gödel
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 connait des listes finies et complètes de tous ses principes.
Nous allons donner plusieurs définitions équivalentes de cette notion de complétude.
| Sommaire |
Diverses formulations équivalentes du théorème de complétude
On peut donner un nombre 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 d’une preuve est précisée par la théorie des modèles. 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 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 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.
Donnons d’abord de ce théorème plusieurs formulations équivalentes.
Il faut quelques définitions : conséquence logique, prouvabilité, cohérence et incohérence dans un système logique, possiblement et absolument vrai et faux.
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.
On peut remarquer qu’il y a une circularité dans cette définition, au sens où on ne peut pas la comprendre si l’on ne sait pas déjà ce qu’est une conséquence logique. Le but d’une telle définition n’est pas d’apprendre au lecteur ce qu’est une conséquence logique. On suppose qu’il le sait déjà, ou qu’il en a une idée, peut-être un peu vague. Le but ici est seulement de préciser une notion intuitive, de lui donner une formulation sans équivoque.
Si p et q sont deux formules du calcul des prédicats, q est prouvable à partir de p dans un système logique L, lorsqu’il existe une preuve de q à partir de p dans L, au sens où les règles de déduction de L suffisent pour déduire q en un nombre fini d'étapes à partir de p et des axiomes logiques de L.
Une formule p est cohérente dans L lorsque pour toute formule q, (q et non q) n’est pas prouvable à partir de p dans L.
Une formule p est incohérente dans L lorsqu’il existe une formule q telle que (q et non q) soit prouvable à partir de p dans L.
Une formule p du calcul des prédicats est possiblement vraie lorsqu’elle est vraie dans au moins un modèle. Elle est absolument vraie, ou est une loi logique, lorsqu’elle est vraie dans tous les modèles. Elle est 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.
On peut alors énoncer le théorème de complétude sous la forme suivante.
Il existe des systèmes logiques valides L qui satisfont aux trois conditions équivalentes suivantes.
(i) 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.
(ii) pour toute formule p, si p est cohérente dans L alors p est possiblement vraie.
(iii) pour toute formule p, si p est absolument fausse alors p est incohérente dans L.
La déduction naturelle ne contient pas d'axiomes logiques ou de schémas d'axiomes mais seulement des règles de déduction. On peut alors définir les vérités anhypothétiques comme les formules prouvables, en un nombre fini d'applications des quinze règles, à partir d'aucune hypothèse. Dans ce cas particulier, on peut alors donner au théorème de complétude la forme suivante.
Pour toute formule p, si p est absolument vraie alors p est une vérité anhypothétique.
Ou encore.
Pour toute formule p, si p est absolument fausse alors (non p) est une vérité anhypothétique.
Il faudra prouver au préalable que la déduction naturelle est un système logique valide, ce qui reviendra à prouver que si p est une vérité anhypothétique alors p est absolument vraie, pour toute formule p (du calcul des prédicats du premier ordre).
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 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, ou plus précisément.
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 possiblement fausses n'est pas énumérable, ou, de façon équivalente, l'ensemble des formules possiblement vraies n'est pas énumérable. Cela revient à dire que l'imagination déborde tous les cadres. Voir aussi Incomplétude
Une preuve
Elle passe par plusieurs étapes.
La validité du calcul des prédicats du premier ordre
Le calcul des prédicats est valide au sens où si une formule c est déductible avec les règles de la déduction naturelle à partir d'une formule h alors c est une conséquence logique de h, au sens de la théorie des modèles, rappelé ci-dessus.
Pour le prouver, il est plus commode d'énoncer les règles de déduction sur un calcul de séquences inventé par Gerhard Gentzen.
Une séquence est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion.
Montrons que toutes les séquences prouvables sont valides.
Une séquence est prouvable si elle est ou bien un axiome, ou bien déduite des axiomes par un nombre fini d'applications des règles de la déduction naturelle des séquences. Les axiomes sont ici toutes les séquences de la forme (p implique p) où p est une formule du calcul des prédicats. Ils sont évidemment 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équences valides, on ne peut déduire que des séquences valides si on applique une des règles de la déduction naturelle des séquences. Le principe d'induction complète suffit alors pour conclure que toutes les séquences prouvables sont valides.
La façon dont les règles de calcul ont été formulées montre que si la formule c est déductible à partir de h avec les règles de la déduction naturelle alors (h implique c) est une séquence prouvable, donc valide. Cela termine cette preuve de la validité des règles de la déduction naturelle.
On peut aussi en déduire que les vérités anhypothétiques sont absolument vraies. Si p est une vérité anhypothétique alors (silence implique p) est une séquence prouvable, donc valide. Comme silence est vrai dans tous les modèles, p est absolument vraie.
La complétude du calcul des propositions
Nous montrerons plus loin que tout système d'axiomes du calcul des prédicats peut être remplacé par un autre système d'axiomes du calcul des propositions qui lui est essentiellement équivalent. Nous aurons alors besoin du théorème de complétude du calcul des propositions (démontré par Paul Bernays en 1926.
Les formes prénexes normales
Une formule du calcul des prédicats est toujours équivalente à une formule mise sous forme prénexe normale, 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.
La construction 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 possiblement vraie.
Cohérente veut dire qu'aucune contradiction n'est prouvable si on prend cette formule comme hypothèse.
En fait nous prouverons une version renforcée de ce théorème.
Si un ensemble d'axiomes est cohérent alors il est possiblement vrai.
Un ensemble d'axiomes est cohérent lorsqu'aucune contradiction n'est prouvable à partir d'un nombre quelconque, fini, de ces axiomes. Il est possiblement vrai lorsqu'il y a un modèle dans lequel les axiomes sont tous vrais. Cette version renforcée nous servira pour énoncer le paradoxe de Skolem.
Commençons par montrer comment remplacer un système d’axiomes du calcul des prédicats par un système d’axiomes du calcul des propositions d’une façon telle que la possibilité de la vérité de l’un soit équivalente à la possibilité de la vérité de l’autre, au sens où si l’un a un modèle, l’autre aussi. Pour cela, il faut mettre chaque axiome sous une forme prénexe normale.
On introduit alors 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 (pour tout x)(il existe un y tel que x+y = 0) est remplacé par (pour tout x) (x+(-x) = 0) où - est un nouvel opérateur unaire.
Pour un axiome de la forme (pour tout x)(pour tout y)(il existe un z tel que Pxyz), on introduit un opérateur binaire, * par exemple, et on prend pour axiome (pour tout x)(pour tout y)( Pxy(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. Deux noms x et y nomment le même être si et seulement si la formule x = y est prouvable à partir des axiomes.
L’ensemble des formules atomiques est obtenu à partir de l’ensemble des noms d’objets et des prédicats fondamentaux mentionnés dans les axiomes.
Chaque axiome prénexe sans quantificateurs existentiels peut être considéré comme un schéma d’axiomes. On supprime tous les quantificateurs universels et on remplace toutes les variables alors libres par des noms d’objet. On obtient ainsi un ensemble infini de formules du calcul des propositions. La réunion de toutes ces formules est le nouveau système d’axiomes, non quantifiés, destiné à remplacer le système d’origine.
Cet ensemble d’axiomes est en général infini. Il est possiblement vrai lorqu’il y a un modèle dans lequel tous les axiomes sont simultanément vrais.
Comme une formule est équivalente à sa forme prénexe. Le système d’axiomes prénexes est équivalent au système d’axiomes d’origine. Si le système d’axiomes prénexes est vrai dans un modèle alors on peut interpréter dans ce modèle les fonctions que nous avons introduites et les axiomes sans quantificateurs existentiels sont alors vrais dans ce même modèle. Inversement si ces derniers sont vrais dans un modèle alors les axiomes prénexes le sont aussi.
Si les axiomes sans quantificateurs existentiels sont vrais dans un modèle, ils sont nécessairement vrais dans un modèle M défini sur U. Comme tous les axiomes non-quantifiés sont des conséquences logiques (par la règle de singularisation) des précédents, ils sont donc tous vrais dans M. Inversement, s’il y a un modèle M tel que tous les axiomes non-quantifiés y soient vrais, alors les axiomes quantifiés le sont aussi, par définition de la vérité des formules quantifiées.
La possibilité de la vérité du système d’axiomes d’origine, ou sa satisfiabilité dans un modèle, est donc équivalente à la satisfiabilité du système d’axiomes non-quantifiés.
Supposons que le système d’axiomes d’origine soit absolument faux alors le système d’axiomes non-quantifiés l’est aussi. Si tous les sous-ensemble finis des ces axiomes étaient possiblement vrais alors le système complet serait possiblement vrai, d’après le théorème de compacité. Il y a donc un sous-ensemble fini de ces axiomes qui est absolument faux. La conjonction C de tous ces axiomes est elle aussi absolument fausse. D’après le théorème de complétude du calcul des propositions sa négation non C est une vérité anhypothétique.
Mais C peut être déduit avec les règles de la déduction naturelle d’une conjonction A d’un nombre fini d’axiomes d’origine. (si A alors C) est donc une vérité anhypothétique. On en déduit que (si (non C) alors non A) est une vérité anhypothétique, parce que la règle de contraposition est une règle dérivée. non A est donc une vérité anhypothétique, par la règle de détachement. On a ainsi prouvé une forme renforcée du théorème de complétude.
Si un système d’axiomes est absolument faux alors il existe une conjonction d’un nombre fini d’axiomes dont la négation est une vérité anhypothétique.
Cette forme renforcée nous servira pour exposer le paradoxe de Skolem, parce qu’elle permet d’appliquer le théorème de complétude à des systèmes infinis d’axiomes.
Le théorème de König, tout arbre infini à branchement fini a une branche infinie, est au cœur de cette preuve du théorème de complétude, par l'intermédiaire du théorème de compacité.
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 a un modèle alors il a un modèle dénombrable.
Skolem a compris que ce théorème est très paradoxal. Il avait montré qu'on pouvait développer une théorie des ensembles à partir d'un ensemble infini dénombrable d'axiomes. Il en suffit d'un petit nombre, moins d'une dizaine, et d'un schéma d'axiomes, qui détermine de façon mécanique un ensemble infini d'axiomes. On peut choisir le schéma d'axiomes de séparation de Ernst Zermelo ou le schéma d'axiomes de remplacement de Abraham Fraenkel. Celui-ci est plus puissant que le précédent et permet, avec les autres axiomes de Zermelo, et l'axiome du choix, de prouver tous les grands théorèmes de Georg Cantor sur les ensembles infinis.
Le théorème de Löwenheim affirme alors que si la théorie ZFC (Zermelo, Fraenkel, axiome du Choix) a un modèle alors elle a un modèle dénombrable. C'est paradoxal, parce que ZFC permet de prouver les théorèmes de Cantor sur l'existence des ensembles indénombrables. Autrement dit, si ZFC est cohérente, il existe un univers dénombrable d'ensembles dans lequel il y a du sens à affirmer l'existence d'ensembles indénombrables. Mais la théorie ne peut remplir ces ensembles qu'avec un nombre dénombrable d'éléments. La théorie affirme que ces ensembles sont indénombrables mais elle ne les remplit pas assez pour justifier cette affirmation. Tel est le paradoxe de Skolem.
La notion d'incomplétude ontologique est reliée au paradoxe de Skolem. Dès qu'on veut nommer tous les éléments des ensembles qu'on définit, on n'a que des ensembles dénombrables. Cela n'empêche pas de nommer des ensembles indénombrables, mais on ne peut pas alors espérer les remplir complètement. Il faut se contenter de résultats partiels, qui comprennent tout de même tous les théorèmes de Cantor et de beaucoup d'autres, et qui ensemble forment ce que David Hilbert a appelé un paradis.
Les modèles non-standards
Si on applique la construction d'un modèle telle qu'elle est définie dans la preuve de complétude, on obtient en général un modèle non-standard. Pour préciser cette notion, raisonnons sur l'arithmétique formelle.
Gödel a prouvé (théorème d'incomplétude de Gödel) que les formules prouvables à partir des axiomes de l'arithmétique formelle ne peuvent être toutes les formules vraies. Autrement dit, il y a des formules vraies à propos des nombres entiers, mais non-prouvables à partir de ces axiomes. On peut alors concevoir des modèles non-standards de l'arithmétique formelle. Ce sont des modèles, au sens où tous les axiomes et toutes leurs conséquences y sont vrais, mais ils sont non-standards parce qu'il y a des formules vraies pour les entiers qui ne sont pas vraies dans ces modèles et inversement.
Abraham Robinson et d'autres ont montré, en développant ce qu'on appelle aujourd'hui l'analyse non-standard, que de tels modèles de l'arithmétique permettent de formaliser des intuitions de Leibniz sur l'infiniment petit.
Chacun est libre de choisir ses axiomes. Si une théorie a besoin de nouveaux axiomes pour apporter des résultats nouveaux, il ne faut surtout pas l'en priver. Cela ne doit pas cependant faire croire qu'on peut mettre sur un pied d'égalité les vérités arithmétiques standards et non-standards. Montrons-le sur un exemple.
Il se pourrait que le théorème de Fermat-Wiles ne soit pas prouvable sur la base des seuls axiomes de l'arithmétique formelle. La preuve d'Andrew Wiles se sert des axiomes de la théorie des ensembles. Si tel était le cas, on pourrait trouver un modèle non-standard dans lequel le théorème de Fermat est faux. Bien sûr cela n'enlèverait rien à la valeur de la preuve de Wiles, parce que la vérité du théorème est définie relativement aux entiers ordinaires et non relativement aux modèles non-standards.
Les modèles non-standards peuvent être très utiles pour donner des preuves d'indépendance et de cohérence entre axiomes.
Autres axiomatisations du calcul des prédicats du premier ordre
Conclusion : la fiabilité de la logique classique du premier ordre
Voir aussi
Sources
- Raymond Smullyan, First order logic 1968 (un exposé moderne) ISBN 0486683702
- Kurt Gödel, Collected works, vol 1 (la thèse de Gödel Sur la complétude du calcul logique 1929, l'article qui a suivi La complétude des axiomes du calcul des fonctions 1930,...) ISBN 0195039645
- Alonzo Church, Introduction to mathematical logic 1956 (Un formalisme précis mais pas toujours convivial. Sur certains sujets, il reste l'un des meilleurs exposés.) ISBN 0691029067