Théorème d'incomplétude de Gödel
Un article de Freepedia.
Le premier théorème d'incomplétude de Gödel (parfois appelé simplement théorème de Gödel) a été prouvé par Kurt Gödel en 1930, et publié en 1931 dans son article fondateur Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme (Sur l'indécidabilité formelle des Principia Mathematica et des systèmes apparentés).
Enoncés des deux théorèmes
Le premier théorème d'incomplétude peut être énoncé de la façon suivante.
Dans n'importe quel système finiment axiomatisé cohérent et capable de formaliser l'arithmétique, on peut construire une proposition qui ne peut être ni prouvée ni réfutée dans ce système.
- De telles propositions ou énoncés sont appelés indécidables du système.
La preuve de ce théorème est immédiatement suivie (dans l'article de 1931) de la preuve d'un second théorème d'incomplétude.
Si T est une théorie cohérente, tout énoncé de T qui affirme la cohérence de T est un indécidable de T.
Ces théorèmes ont été prouvés sous des conditions très générales, remplies par toutes les théories destinées à fonder les mathématiques, telles que les Principia Mathematica, de Whitehead et Russell et les systèmes apparentés.
Une théorie est cohérente si aucune contradiction ne peut être prouvée à partir de ses axiomes. On dit aussi qu'elle est consistante, ou non-contradictoire.
Une théorie est finiment axiomatisée si on peut donner une liste finie de ses axiomes ou de ses schémas d'axiomes.
La relativité de l'indécidabilité des énoncés
Le théorème ne prétend pas pour autant l'existence d'indécidables « absolus », c'est-à-dire indémontrables dans n'importe quel système formel. En effet, il est toujours possible d'ajouter un axiome à un système formel dans le but de rendre un indécidable démontrable dans le nouveau système.
On pourrait penser « s'échapper » du théorème d'incomplétude en construisant un système formel où les indécidables seraient progressivement « résolus » avec de nouveaux axiomes. Mais le nouveau système ainsi créé remplirait encore les conditions des théorèmes de Gödel, pourvu que ses axiomes soient en un sens calculables (liste récursivement énumérable d'axiomes). Il comporterait alors lui aussi des indécidables, et serait donc toujours incomplet.
On peut directement déduire du second théorème que la démonstration de la cohérence de l'arithmétique en utilisant uniquement les axiomes de l'arithmétique, sans utiliser par exemple les axiomes de l'infini et les autres axiomes de la théorie des ensembles, comme l'avait suggéré David Hilbert, est impossible. Mais la cohérence de l'arithmétique peut tout de même être prouvée, de plusieurs façons.
Gerhard Gentzen a donné une preuve de consistance après avoir développé des méthodes d'analyse des théories définies par récurrence et en se fondant sur une induction transfinie jusqu'au petit ordinal dénombrable ε0. Cette preuve met à profit toute la puissance du raisonnement par récurrence mais elle raisonne toujours sur des ensembles « bien construits ».
Sans utiliser les méthodes de Gentzen, qui ont été ensuite développées dans la théorie de la preuve, on peut donner une preuve naturelle, simple, élémentaire, de la cohérence des axiomes de l'arithmétique formelle en se servant de la théorie des modèles. Mais cette preuve ne peut pas être formalisée à l'intérieur de l'arithmétique formelle. Elle présuppose notre capacité à connaître les ensembles infinis définis par récurrence et la validité générale du principe d'induction complète. De tels présupposés reviennent à reconnaître la validité de certaines constructions ensemblistes élémentaires.
Cette preuve ne prouve donc pas la validité du principe d'induction complète puisqu'elle la présuppose, mais elle prouve que la forme qui lui est donnée dans l'arithmétique formelle est sans danger, qu'elle ne peut pas conduire à une contradiction. Elle est convaincante dans la mesure où on est déjà convaincu que les raisonnements sur certains ensembles infinis sont valides.
On peut s'échapper des conditions du premier théorème d'incomplétude en adoptant comme axiomes toutes les vérités de l'arithmétique formelle. Mais un tel système d'axiomes, quoique très bien défini, ne peut pas être finiment axiomatisé, au sens où aucun système finiment axiomatisé ne lui est équivalent - finiment axiomatisé ne veut pas dire que le nombre des axiomes, c'est à dire les formules initiales des preuves, est fini, mais que les principes des axiomes sont en nombre fini : nombre fini de schémas d'axiomes, ou plus généralement, liste infinie et récursivement énumérable d'axiomes. Mais ce système est complet. On peut y prouver toutes les vérités puisqu'elles sont toutes des axiomes.
Des exemples de systèmes incomplets et d'indécidables
Qu'une théorie soit incomplète n'est a priori pas étonnant. Il suffit qu'elle ne contienne pas assez d'axiomes. Mais que l'arithmétique formelle et les Principia Mathematica soient incomplets était beaucoup plus étonnant. Dans le projet logiciste des auteurs des Principia, leur système devait contenir tous les axiomes dont on a besoin pour toutes les preuves mathématiques.
Le problème de l'incomplétude s'était déjà posé à propos de la géométrie. Jusqu'aux travaux de Gauss, de Lobatchewsky, puis de Riemann, on pouvait croire que l'axiome des parallèles pourrait être prouvé à partir des autres axiomes de la géométrie euclidienne, qui définissent la géométrie absolue. En cherchant des preuves de cet axiome, certains se sont rendus compte que la négation de l'axiome des parallèles pouvait conduire à des résultats intéressants. Cela a conduit aux développements des géométries non-euclidiennes. Cela a montré que l'axiome des parallèles n'est pas déductible à partir des autres axiomes d'Euclide. Autrement dit, la géométrie absolue est incomplète. L'axiome des parallèles est pour elle un indécidable. On peut le prouver (Beltrami 1868) en donnant un modèle de la géométrie absolue (les droites sont les grands cercles d'une sphère, les points sont les couples de points diamétralement opposés sur la sphère) pour lequel tous les axiomes de la géométrie plane sont vrais, sauf l'axiome des parallèles.
Le théorème d'incomplétude donne une méthode mécanique pour créer des indécidables, si bien que les logiciens ont pu construire de nombreux indécidables. Mais ces énoncés sont créés « artificiellement » et ne répondent pas toujours à des interrogations réelles des mathématiciens.
Quand on se donne une théorie suffisamment riche en axiomes (l'arithmétique formelle ou une théorie des ensembles), on pourrait croire que les énoncés vrais mais non prouvables sont toujours des formules très compliquées, construites avec des techniques logiques paradoxales, qui n’interviennent jamais dans les mathématiques couramment étudiées. Autrement dit, on pourrait espérer que l’incomplétude est seulement marginale et qu’elle ne concerne pas les questions mathématiques importantes. Mais ce jugement est erroné, on peut donner de nombreux exemples.
Paul Cohen a prouvé qu’une conjecture de Cantor, l’hypothèse du continu, n’est pas prouvable à partir des axiomes de la théorie ZFC des ensembles. Cela seul suffit pour montrer que l’improuvabilité est une question qui se pose vraiment.
Mais elle se pose aussi pour des problèmes plus élémentaires. Nous allons voir qu'elle se pose à propos des équations diophantiennes par exemple.
On peut donner un sens absolu à la notion d'indécidabilité, non à propos des énoncés, mais des ensembles d'énoncés, ou problèmes. Un ensemble d'énoncés est indécidable s'il n'existe pas de théorie finiment axiomatisée qui permette de répondre pour tous les énoncés si oui ou non ils sont vrais. On ne prétend pas qu'il y a des énoncés dont la vérité ne peut pas être connue mais seulement qu'il n'existe pas de méthode unique et mécanisable qui suffise pour répondre à toutes les questions.
Les axiomes de l'arithmétique formelle, ou de toute autre théorie finiment axiomatisée, ne suffisent pas pour la résolution de toutes les équations diophantiennes (savoir si une équation algébrique à coefficients entiers a des solutions en nombres entiers et si non le prouver). Le théorème de Matiyasevich dit que ce problème est indécidable. Les axiomes de l'arithmétique formelle suffisent pour trouver toutes les solutions, mais ils ne suffisent pas pour prouver pour toutes les équations qui n'ont pas de solutions qu'elles n'en ont pas. Autrement dit, il y a des formules arithmétiques composées d'une unique équation diophantienne, niée, et précédée de quantificateurs universels sur toutes ses variables, qui sont vraies mais qui ne sont pas prouvables à partir des axiomes.
Un exemple célèbre d'équation diophantienne est le théorème de Fermat-Wiles. On ne sait pas s'il est un énoncé indécidable de l'arithmétique formelle, ayant été prouvé par Andrew Wiles dans la théorie des ensembles.
Un autre exemple est les équations de Grégory Chaitin, qui ne possèdent pas moins de 12000 variables, et qui possèdent soit une infinité de solutions soit un nombre fini. Chaitin a montré que dans n'importe quel système formel on ne peut résoudre qu'un nombre fini de ces équations, les autres étant des indécidables du système en question.
D'autres exemples de problèmes indécidables sont donnés dans l'article indécidabilité.
La mise en cause du mouvement formaliste
Pour répondre aux problèmes de la crise des fondements des mathématiques, Hilbert et ses élèves avaient espéré que des méthodes formalistes apporteraient une réponse complète et définitive aux problèmes des fondements des mathématiques, en donnant une procédure mécanique, un algorithme, destiné à répondre à toutes les questions formelles (voir Fondation des mathématiques).
On peut déduire du premier théorème d'incomplétude de Gödel que ce programme de Hilbert n'est pas réalisable, du moins pas sous sa forme initiale. On connait cependant de nombreuses théories décidables. Elles ne suffisent pas pour toutes les mathématiques mais présentent parfois un grand intérêt. Tarski a donné un algorithme de décision pour la géométrie euclidienne élémentaire (la géométrie sans axiome sur la continuité de l'espace).
Le théorème d'incomplétude en philosophie
- Souvent cité en philosophie. Il faut pourtant faire très attention à son utilisation hors du champ des mathématiques, car l'utilisation du théorème d'incomplétude doit être basée sur un système formel. De plus, comme nous l'avons dit, des indécidables absolus n'existent pas, si bien que toute tentative de démontrer par exemple que l'existence de dieu est un indécidable absolu serait vaine.
- Les théorèmes d'incomplétude montrent qu'il n'est pas possible de donner une liste finie et formalisée de tous les principes à partir desquels on peut développer une preuve mathématique. On peut toujours imaginer d'aller au de-là de ce qui est permis par les axiomes. Ces théorèmes montrent que l'imagination déborde tous les cadres. (voir incomplétude)
- On les interprète parfois comme des signes d'impuissance de la raison. Cette interprétation doit être prise avec précaution. Ces théorèmes manifestent la puissance de l'imagination et la capacité de la raison à reconnaître ses limites, à reconnaître son incapacité à enfermer l'imagination dans des limites fixées une fois pour toutes, comme un cheval dans un enclos trop petit. En outre ils ne mettent pas en doute la possibilité de connaître tous les principes logiques valides (voir théorème de complétude), si l'on limite la logique au calcul des prédicats du premier ordre.
Une preuve partielle du premier théorème d'incomplétude
La preuve du premier théorème d'incomplétude de Gödel est, comme celle du théorème d'incomplétude de Tarski, fondée sur le paradoxe du menteur.
Les énoncés paradoxaux sont produits par une technique logique très générale qui consiste à représenter les formules d’une théorie T par des objets de T. C’est possible dès que T contient les nombres entiers positifs parmi ses objets. Gödel et ses successeurs ont inventé des techniques de codage, de numérotation, qui permettent de représenter n’importe quelle formule par un entier, de telle façon que chaque entier représente au plus une formule.
Gödel a alors inventé la notion de prédicat de prouvabilité.
Un prédicat de prouvabilité pour une théorie T est une formule à une variable x qui est vraie si et seulement si x représente un théorème de T, c’est-à-dire une formule démontrable à partir des axiomes de T.
Gödel a prouvé qu’une théorie mathématique T vraie et suffisamment riche remplit la condition suivante.
Pour toute théorie axiomatique T’ (finiment axiomatisée), il existe dans T un prédicat de prouvabilité pour T'
Finiment axiomatisée veut dire que les axiomes, les schémas d'axiomes et les règles de déduction sont en nombre fini.
En particulier, T contient un prédicat de prouvabilité pour elle-même. Même l’arithmétique formelle est capable de représenter ainsi toutes les théories axiomatiques. En ce sens on peut la voir comme une théorie universelle. Il suffit de savoir raisonner sur les nombres pour définir toutes les théories concevables. Les nombres peuvent être considérés comme les atomes, les principes premiers de la raison, au sens où tout le reste peut être construit à partir d’eux. Il y a quelque chose de pythagoricien, tout est nombre, dans cette approche gödelienne des mathématiques.
La preuve de l’existence d’un prédicat de prouvabilité est un peu difficile quand on représente des formules par des nombres.
A partir du théorème de Tarski et de l’existence d’un prédicat de prouvabilité on peut déduire le premier théorème d’incomplétude de Gödel comme une conséquence directe.
Une théorie axiomatique, vraie et suffisamment riche, ne peut pas prouver toutes ses formules vraies.
Cette formulation est un peu différente, mais équivalente à celle qui a été présentée au début de cet article. Elle recourt à la notion de vérité dans un modèle.
Ce théorème peut être considéré comme un corollaire de celui de Tarski. Mais Gödel est le premier à avoir publié ses preuves. Tarski a eu les mêmes intuitions au même moment.
La preuve de Gödel ne recourt pas au théorème de Tarski mais elle est semblable à celle de Tarski, sauf qu’il ne se sert pas d’un prédicat de vérité mais d'un prédicat de prouvabilité Px dont il a montré auparavant l’existence, ainsi que celle du prédicat de substitution SUBxyz. (voir théorème d'incomplétude de Tarski).
Gödel considère alors la formule (il existe un z tel que SUBxxz et non Pz). Elle est représentée par un nombre n de T. Il y a aussi un autre nombre KG tel que SUBnn(KG). n et (KG) sont des nombres bien définis que l’on peut calculer dès que les axiomes de T et le procédé de représentation des formules de T par des nombres sont précisément définis.
Le nombre KG représente-t-il une formule prouvable ?
La formule représentée par KG dit que le prédicat représenté par n est vrai pour n. Le prédicat représenté par n est vrai pour x si et seulement s’il existe un z tel que SUBxxz et non Pz. La formule représentée par KG est donc équivalente à (il existe un z tel que SUBnnz et non Pz) par définition de KG. Or SUBnnz équivaut à z=(KG). Donc par définition de KG, la formule représentée par KG équivaut à non P(KG).
Autrement dit la formule représentée par KG dit d’elle-même qu’elle n’est pas prouvable.
Si on suppose que T est cohérente alors la formule représentée par KG est nécessairement vraie, parce que si elle ne l’était pas, alors elle serait prouvable, T permettrait de prouver une formule fausse et ne serait donc pas cohérente.
Si T est cohérente KG représente un énoncé indécidable de T.
La partie longue de la démonstration de Gödel consiste à définir un prédicat de prouvabilité à l’aide d’une représentation des formules par numérotation. Après les découvertes de Church, Post et Turing, les résultats de Gödel sur la prouvabilité s’inscrivent dans un contexte plus général, celui des ensembles énumérables. L’ensemble des théorèmes, ou formules prouvables, d’une théorie finiment axiomatisée est toujours énumérable.
Argument de la preuve et discussion du second théorème d'incomplétude
Le second théorème d’incomplétude de Gödel affirme que toute théorie mathématique cohérente et suffisamment riche ne peut pas prouver sa propre cohérence. Autrement dit, n’importe quelle technique théorique, qu’elle soit ensembliste ou autre, ne permet jamais de définir une théorie capable de prouver sa propre cohérence, dès lors qu’elle est suffisamment riche pour formaliser l’arithmétique formelle.
La preuve du second théorème est difficile à formaliser mais elle suit assez directement celle du premier.
Si une théorie pouvait prouver sa propre cohérence, c’est qu’elle contient un prédicat de prouvabilité P et le théorème, pour tout x, si x représente une contradiction alors non Px.
Gödel a montré que les théories qu'il étudie permettent de prouver
- P(KG implique x), pour n’importe quelle contradiction représentée par x,
- où (y implique z) est la représentation de la formule qui affirme que la formule représentée par y implique la formule représentée par z.
- si P(y implique z) alors (si Py alors Pz).
On en déduit que si (non Px) était prouvable pour une contradiction représentée par x, alors non P(KG) le serait aussi. Mais ce dernier énoncé équivaut à la formule représentée par KG et la théorie serait contradictoire.
Si la théorie est cohérente, non Px ne peut donc pas être prouvable, pour n’importe quelle contradiction représentée par x. Ces théories, si elles sont cohérentes, ne peuvent donc pas prouver leur propre cohérence.
Les interprétations courantes du second théorème d’incomplétude de Gödel exagèrent souvent sa portée. Gödel a prouvé qu’un certain type de preuve de cohérence ne peut pas exister. Mais il n’a jamais prouvé, ni prétendu avoir prouvé, que des preuves fiables de cohérence sont impossibles.
On propose parfois le raisonnement suivant : la cohérence d’un système X d’axiomes ne peut pas être prouvée avec X. Il faudrait donc un système X+ d’axiomes plus fort que X pour prouver la cohérence de X. Mais la cohérence de X+ serait encore plus douteuse que celle de X, puisqu’il est plus fort. Ce doute invaliderait la preuve. On en conclut parfois à tort que la cohérence des théories mathématiques suffisamment riches ne peut pas être prouvée.
Le raisonnement précédent n’est pas complètement dénué de vérité, parce que le problème de la fiabilité des principes se heurte aux difficultés de la régression à l’infini. À partir de quels principes peut-on prouver la validité des principes ?
Mais le raisonnement ci-dessus ne peut pas non plus être complètement vrai. La cohérence d’un système X d’axiomes est un problème mathématique bien défini. Ou bien il y a une conjonction d’axiomes de X dont la négation est une loi logique, dans ce cas X est incohérent, ou bien non, et X est cohérent. Dans la phrase précédente, toutes les notions (axiome de X, loi logique) peuvent être définies avec précision. Il s’agit donc d’un problème bien défini.
Il n'y a aucune raison valable qui nous permette de penser qu’un problème bien défini puisse être néanmoins insoluble. Les théorèmes sur l’incomplétude et l’indécidabilité portent seulement sur l’inexistence d’une méthode unique et bien définie pour répondre à toutes les questions bien définies.
S’il fallait admettre que la régression à l’infini rend insoluble le problème de la fiabilité des principes alors même les méthodes les plus élémentaires devraient être suspectées. On ne pourrait même pas être sûr que les opérations arithmétiques d’addition et de multiplication fournissent toujours un résultat bien défini.
L’erreur dans le raisonnement ci-dessus consiste à admettre que la cohérence de X+ est plus douteuse que celle de X. Tant qu’on se limite à des théories élémentaires, on n’a en vérité pas de doutes sur la validité de nos principes de preuve.
Les doutes sur la fiabilité des principes et le problème de la régression à l’infini peuvent être résolus si l’on étudie attentivement la différence entre ce qui est élémentaire et ce qui ne l’est pas en mathématiques.
Sources
- Jean-Paul Delahaye, L'intelligence et le calcul - Belin pour la science, 2002 - ISBN 284245040X
- Jean-Marc Alliot, Thomas Schiex, Pascal Brisset, Frédérik Garcia, Intelligence artificielle & informatique théorique - Cepadues, 2002 - ISBN 2854285786
- Douglas Hofstadter, Gödel, Escher, Bach, les brins d'une guirlande éternelle - Dunod, 2000 - ISBN 210005435X
- Raymond Smullyan, Les théorèmes d'incomplétude de Gödel - Dunod, 2000 - ISBN 210005287X, Theory of formal systems
- Kurt Gödel, Collected works vol 1
- Martin Davis (éd) The undecidable (recueil des principaux articles de Gödel, Church, Turing, Rosser, Kleene, Post)
Voir aussi
- théorème de complétude de Gödel
