Gödel pour les nuls

Le théorème de Gödel pour les nuls

Par David Monniaux le lundi, février 9 2015, 13:08 - Théorie - Lien permanent

Suite à la publication d'un billet où j'évoquais des mystifications autour des théorèmes d'incomplétude de Gödel, on m'a demandé si je pouvais écrire une présentation « grand public » de ceux-ci. C'est ce que je vais tenter ici, en utilisant le moins possible de notations et de jargon mathématiques.

Malheureusement, c'est un sujet qui demande, pour être compris sans contresens, des explications assez conséquentes, et je m'excuse donc d'avance de la longueur de ce billet.

____________________

Comprendre ce que disent les théorèmes d'incomplétude de Gödel demande certaines bases exposées dans cet article, et si vous n'avez pas fait un minimum d'effort pour les acquérir vous ne comprendrez pas ce qu'ils disent. Ce n'est pas un drame, on vit très bien sans.

Kurt Gödel, mathématicien autrichien, s'est intéressé principalement à la logique mathématique et est notamment connu pour ses preuves du théorème de complétude de la logique du premier ordre (sa thèse) et de l'incomplétude de l'arithmétique (son habilitation).

Il n'y a là aucune contradiction !

Je laisse de côté la complétude, et vais me concentrer sur le résultat pour lequel il est le plus souvent cité par les non-spécialistes, à savoir l'incomplétude. Ces résultats mettant en jeu la notion de « preuve », je vais donc commencer par expliquer ce qu'est une preuve en mathématiques.

La preuve mathématique

En mathématiques,

• une preuve, ou démonstration, est un texte censé montrer qu'une conclusion s'ensuit de certaines hypothèses.
• Un théorème est un énoncé mathématique qui a été démontré,
• par opposition à une simple conjecture.

Dans l'immense majorité des cas, une preuve est un texte en langue naturelle (anglais, français) mêlé de notations mathématiques. Le style d'écriture est assez codifié et convenu.

Prenons un exemple concret (qu'il ne sera pas utile de comprendre) : le théorème bien connu depuis l'antiquité que « la longueur de l'hypoténuse d'un triangle rectangle de petits côtés de longueur 1 et 1 ne peut se mettre sous la forme d'une fraction d'entiers a/b » ; autrement dit « racine de 2 est irrationnel ».

Supposons que l'on ait deux entiers naturels a et b tels que a/b soit √2, et que a/b soit une fraction irréductible (pas de diviseurs communs à a et b).

Alors a² = 2b². Alors 2 divise a², donc divise a.

On peut donc écrire a sous la forme 2c. Alors il vient 4c² = 2b², donc 2c² = b².

Par le même raisonnement, 2 divise b. Donc 2 est un diviseur commun à a et b, ce qui est absurde.

Il s'agit d'une preuve par l'absurde : pour démontrer que quelque chose n'est pas vraie, on suppose qu'elle est vraie, et on arrive à une contradiction.

cette preuve recèle certaines étapes implicites, certains non-dits

Ainsi, nous aurions dû partir de l'hypothèse « Supposons que l'on ait deux entiers naturels a et b tels que a/b soit √2 » et non lui adjoindre l'hypothèse que a/b est irréductible. C'est qu'il est bien connu que toute fraction peut être transformée en une fraction irréductible de même valeur… donc s'il existe une fraction comme j'ai dit, il en existe une irréductible.

Ensuite,

• j'ai utilisé le fait que si un nombre premier (ici 2) divise le carré d'un autre nombre (ici a), alors il divise ce nombre.
• J'ai réarrangé des égalités (par exemple transformer a/b = √2 en a² = 2b²).
• J'ai sauté une partie du raisonnement en disant qu'elle est identique (en changeant ce qui doit l'être) à une partie déjà écrite plus haut.

=>De fait, une preuve mathématique s'adresse à un public censé être capable, dans une certaine mesure, de « compléter les trous » notamment en appliquant sans qu'on lui fasse remarquer des résultats « bien connus ».

La forme de sa rédaction dépend donc du public visé :

• un mathématicien professionnel s'adressant à d'autres mathématiciens du même domaine dans une revue de recherche peut se permettre des raccourcis
• qu'on ne se permettrait pas dans un cours de lycée.

Ces raccourcis sont nécessaires pour limiter la longueur de la preuve et la garder lisible.

Cas où tout est décrit

À l'inverse, il existe une notion de preuve formelle où toutes les étapes sont explicitement décrites, sans « raccourcis ».

Une telle preuve ne demanderait ni intelligence ni connaissances spécifiques (hors la liste des théorèmes déjà connus) pour être vérifiée : il suffit de vérifier que les théorèmes sont correctement cités, que les règles de la déduction logique sont correctement appliquées (si on a démontré que A implique B, et qu'on a A, alors on a le droit de déduire B mais pas de déduire C…).

Si l'on utilise des notations entièrement symboliques, et non une langue naturelle, la vérification qu'un texte est bien une preuve formelle correctement formée peut se faire par un programme informatique.

Présupposé idéologique

Les mathématiciens professionnels travaillent généralement avec le présupposé idéologique que, s'ils en faisaient l'effort, ils pourraient traduire leurs preuves en langue naturelle en preuves formelles, mais qu'ils ne le font pas parce que c'est trop fastidieux.

De fait, une preuve formelle peut souvent ressembler à une liste d'instructions de GPS pour se rendre d'un point à un autre (« tournez à gauche », « tournez à droite », « faites 1 km sur la départementale 506 »...) : ça n'a pas la clarté d'une explication comme « quittez Grenoble et allez à Voiron par l'autoroute ».

Remarques :

• Une preuve mathématique informelle est écrite par des mathématiciens à destination d'autres mathématiciens :

• outre son contenu « probant »,
• elle peut ou non transmettre des intuitions, des idées, qui pourront être utilisées dans d'autres contextes.

• Noyer le lecteur sous des détails nuit à cette transmission.

La notion de calcul

On pourrait objecter à mes explication ci-dessus un certain anachronisme :

Comment un théorème prouvé en 1931 pourrait-il sous-entendre une notion de programme informatique, alors que celle-ci date d'après la Seconde guerre mondiale ?

C'est qu'à l'époque, on s'interrogeait sur la notion de calcul, c'est-à-dire de ce que pourrait faire un calculateur complètement stupide, dénué d'intelligence ou d'intuition, mais doté d'une infinie patience, d'une parfaite fiabilité, et d'une quantité indéfinie de temps et de papier pour écrire.

En 1900, le fameux mathématicien David Hilbert posait une série de grande « problèmes » dont il estimait que l'étude ferait considérablement avancer les mathématiques.

Le dixième problème réclamait un « procédé » pour résoudre un certains types d'équations (les équations diophantiennes, dont la définition importe peu ici).

Comprenons bien la difficulté ici. On connaît depuis l'Antiquité des procédés de calcul, par exemple l'algorithme d'Euclide. En lisant leur description, on comprend pourquoi un calculateur stupide peut les appliquer. Suite à des questions posées au début du XXe siècle, notamment celles de Hilbert, on a fini par se dire que si l'on ne connaissait pas de procédé de calcul pour certaines questions, c'est parce qu'il n'en existe pas.

Or, en mathématiques, pour montrer que quelque chose n'existe pas, on ne peut pas se contenter d'énumérer une liste de tentatives infructueuses pour le trouver : on doit partir d'une définition de la chose et montrer que celle-ci conduit à une contradiction. Il a donc fallu dégager une définition du « calcul ».

Ce sont ces recherches qui ont notamment abouti sur la notion de machine proposée par le jeune Alan Turing.

En 1931, donc, la notion formelle de calcul est déjà dans l'air, mais en revanche on n'a pas encore de machine concrète susceptible de la mettre en œuvre, même s'il y a déjà du calcul mécanisé. Ce n'est que bien plus tard que l'on a pu réaliser des outils informatiques (dits « assistants de preuve ») susceptibles de vérifier effectivement des preuves mathématiques formelles non ridiculement petites, et encore, ces outils sont difficiles d'emploi.

Notons au passage que le dixième problème de Hilbert n'a trouvé de réponse qu'en 1970. Les questions mathématiques profondes peuvent exiger des dizaines, voire des centaines d'années, pour leur résolution.

Les systèmes d'axiomes

Le programme informatique qui vérifie qu'une preuve est correcte doit vérifier deux critères :

• Les connexions logiques sont correctement utilisées. Par exemple, on a le droit de conclure qu'on a prouvé A et B si l'on a prouvé A et l'on a prouvé B, mais pas si l'on a prouvé A et prouvé C.

• Les axiomes utilisés dans la preuve sont valides.

Voyons ceci de plus près.

Une preuve mathématique part de certains faits admis sans démonstration, dits axiomes. Ces faits sont en quelques sortes des « évidences » en les quelles le mathématicien croit en ce qui concerne la classe d'objets sur lesquels il veut raisonner.

Par exemple, on peut donner une liste d'axiomes, dits parfois « axiomes d'Euclide », sur lesquels construire la géométrie plane, qui rapportent des faits de base comme « entre deux points on peut toujours tracer une ligne droite ».

La liste des axiomes admis constitue en quelque sorte une « règle du jeu mathématique » :

• on peut travailler à partir d'axiomes différents de ceux communément utilisés,
• mais il faut le dire franchement avant de donner sa preuve.

Le programme de vérification des preuves va prendre chaque axiome et vérifier s'il est valide. Dans certains cas, il est nécessaire d'admettre comme valides une infinité d'axiomes, et donc le programme ne pourra pas se référer à une liste de longueur finie ; ce qui importe, c'est alors seulement qu'il réponde toujours par « valide » ou « invalide » au vu d'un axiome.

On dit alors que la théorie mathématique définie par le système d'axiomes est récursivement axiomatisable.

Les théorèmes d'incomplétude de Gödel portent sur des systèmes récursivement axiomatisables.

Comment s'accorde-t-on sur un système d'axiomes ?

On a parfois l'impression que les axiomes « tombent du ciel ». En réalité, ils sont le résultats d'un processus historique et social. Des mathématiciens étudiaient tel ou tel concept intuitif (par exemple, les nombres entiers, ou la géométrie dans le plan), et ont tenté de dégager des listes d'axiomes décrivant ces concepts. Ils se sont trouvés alors pris en tenaille par deux difficultés antagonistes : l'incomplétude et la contradiction.

contradiction 

Si l'on choisit mal un système d'axiomes, celui-ci peut permettre de démontrer à la fois une chose et son contraire, d'où la contradiction. Un systèmes d'axiomes contradictoire n'a aucun intérêt parce qu'avec lui tout est démontrable, même les choses les plus intuitivement absurdes. C'est donc un défaut majeur.

Par exemple, lorsque l'on a tenté de donner une base à la notion d'ensemble, on a tout d'abord proposé des systèmes d'axiomes qui avaient l'air raisonnables, avant de se rendre compte que ceux-ci permettaient de démontrer une contradiction (dite aussi paradoxe). Plusieurs versions trop naïves de la théorie des ensembles sont ainsi vulnérables au paradoxe de Russell.

minimalité 

On peut aussi vouloir formuler un système d'axiomes minimal : on ne veut pas qu'un quelconque axiome puisse être prouvé à partir des autres. En effet, un tel axiome pourrait être supprimé sans changer quoi que ce soit à ce que l'on peut démontrer avec les axiomes.

complétude 

Une autre propriété intéressante d'un système est qu'il soit complet : quel que soit l'énoncé que l'on puisse écrire dans la théorie,

• soit cet énoncé est démontrable,
• soit son contraire est démontrable.

Un système n'ayant pas cette caractéristique est dit incomplet : on peut écrire des énoncés tels qu'ils ne soient ni démontrables, ni de contraire démontrable. En d'autres termes, le système d'axiomes est insuffisant pour conclure sur ceux-ci.

Il n'y a rien d'extraordinaire à ce qu'un système d'axiomes soit incomplet. Ainsi, je pourrais vouloir axiomatiser ce qui se passe sur un navire et n'avoir rien qui permette de conclure si oui on non l'âge du capitaine est supérieur ou égal à 42.

Plus sérieusement, il est possible de donner une formalisation de la géométrie plane avec un ensemble d'axiomes ne permettant pas de conclure si oui ou non « Par un point donné, on peut mener une et une seule parallèle à une droite donnée ». On dit qu'un tel énoncé (pas de preuve pour lui ni pour son contraire) est indécidable dans le système d'axiomes considéré.

• On peut rajouter cet énoncé comme axiome, auquel cas on obtient une formalisation de la géométrie plane ;
• ou on peut rajouter des axiomes rendant cet énoncé faux, et obtenir une formalisation de la géométrie sur une sphère.

Ainsi, un système incomplet peut être intéressant en ce qu'il exprime les points communs entre diverses théories.

Gödel

Ce qui est significatif dans le résultat de Gödel, c'est que ce qui est démontré incomplet c'est un système d'axiomes pour l'arithmétique sur les entiers, c'est-à-dire un domaine fondamental des mathématiques étudié depuis l'Antiquité. :Mieux, le résultat montre que toute théorie récursivement axiomatisable pour l'arithmétique est forcément incomplète.

Autre remarque 

si un énoncé est indécidable dans un système d'axiomes non contradictoire, c'est qu'on peut aussi bien l'ajouter comme axiome qu'ajouter sa contradiction et qu'on obtient encore un système non contradictoire. Autrement dit, c'est en quelque sorte un énoncé « au choix ».

La décidabilité

Supposons que nous avons affaire à une théorie récursivement axiomatisable ; c'est-à-dire qu'il existe un programme informatique qui reconnaît, au vu d'un énoncé, si c'est ou non un axiome. Alors, nous l'avons vu, il existe un programme informatique qui reconnaît, au vu d'un texte, si c'est ou non une preuve correcte dans ce système d'axiomes.

Si nous voulons savoir si un énoncé est démontrable, il y a donc une méthode évidente et naïve : on prend tous les textes de longueur 1 (A, B, C,…), on regarde si chaque texte est ou non une preuve correcte de l'énoncé recherché, si on n'a pas trouvé on passe aux textes de longueur 2 (AA, AB, AC… BA, BB, BC…), puis de longueur 3 et ainsi de suite. S'il l'énoncé est démontrable, c'est-à-dire qu'il admet une preuve, notre méthode va aboutir quand elle aura trouvé une preuve de longueur minimale de cet énoncé.

Ajoutons que cette approche est une figure de l'esprit. Si on la mettait en œuvre telle quelle sous forme d'un programme informatique fonctionnant sur un vrai ordinateur, la longueur des calculs (leur complexité) serait prohibitive y compris pour retrouver les preuves de théorèmes faciles. C'est une méthode de recherche de preuve particulièrement stupide !

Notons que cette méthode n'aboutit jamais si l'énoncé considéré n'est pas démontrable : le programme « tourne » indéfiniment longtemps.

Si nous sommes sur une théorie complète, nous avons une méthode pour décider si un énoncé est démontrable, ou de contraire démontrable — nous pouvons même dire qu'il s'agit de décider si cet énoncé est « vrai » ou « faux », en nous abstenant de toute considération profonde sur le sens de la vérité : nous énumérons tous les textes par longueur croissante et nous nous arrêtons sur une preuve de l'énoncé ou une preuve de son contraire. Comme la théorie est complète, ce processus aboutit forcément.

À l'inverse, si nous sommes sur une théorie incomplète, présentant des énoncés indécidables, et que nous cherchons à décider un de ces énoncés indécidables, le processus n'aboutira pas. Nous nous retrouvons donc devant le cas intéressant d'un programme informatique dont il serait très intéressant de déterminer s'il terminera ou pas… soit le fameux problème de l'arrêt de Turing !

Rappelons que les méthodes de décision esquissées ci-dessus ne sont pas utilisables en pratique, en raison de leur coût en temps de calcul ou en espace mémoire ; autrement dit très, très vite, elles auraient des besoins prohibitifs. La question de la complexité de la décision de classes de problèmes logiques est centrale en informatique théorique (voir par exemple le problème P=NP, posé dans en 1971 et dont on ignore encore la réponse). Il existe par ailleurs des recherches sur comment décider efficacement en pratique certains types de problèmes (c'est un de mes champs de recherche).

L'arithmétique de Peano

Les entiers naturels (0, 1, 2…) sont des objets mathématiques connus de tous. On apprend d'ailleurs des procédés de calcul (on dit des algorithmes) élémentaires à l'école primaire : comment poser une addition, une multiplication, etc.

Un théorème tel 12×57=684 n'est guère difficile à établir par simple calcul. Plus généralement, les théorèmes du style « pour tout entier x inférieur à 10000000000000, il existe un entier y inférieur à y telle qu'un certain calcul donne 69 » peuvent être décidés par un calcul stupide et exhaustif : on prend tous les xjusqu'à 10000000000000, puis tous les y inférieurs à x, on effectue le calcul… C'est sans doute très mauvais en temps de calcul, mais nous nous autorisons des calculs indéfiniment longs !

En revanche, un théorème de la forme « pour tout entier n... », sans borne sur n, ne peut a priori être établi par simple calcul. La raison est que ce théorème doit être valable pour tout n et qu'il y a un nombre infini de n, donc le calculateur devrait procéder à un nombre infini de vérifications.

Or, ce que recherchent en général les mathématiciens, ce sont des résultats généraux, valables dans tous les cas (ou moyennant un liste exhaustive d'exceptions), pas des cas particuliers calculés un à un. Comment donc s'y prendre pour prouver qu'une propriété est vraie de tout entier, ou de tout couple d'entiers ?

Les mathématiciens ont voulu établir une liste d'axiomes, dits de Peano, décrivant le comportement des entiers : il existe un entier appelé 0, chaque entier a un successeur (au sens où 3 est le successeur de 2, 4 celui de 3…), si deux entiers ont le même successeur alors ils sont égaux, zéro n'est le successeur d'aucun entier, il existe une opération dite « addition » et une dite « multiplication », additionner zéro à un entier redonne le même entier, etc.

Si on sait que quelque chose est vrai de l'entier zéro, et qu'on sait que s'il est vrai pour un entier il est vrai aussi pour son successeur, alors on peut conclure qu'il est vrai pour 1 (successeur de 0), puis pour 2 (successeur de 1). Les axiomes du raisonnement par récurrence permettent de conclure que cela est vrai pour tout n.

Le premier théorème d'incomplétude

Une théorie récursivement axiomatisable, non contradictoire, et capable de représenter l'arithmétique de Peano, est forcément incomplète : elle contient forcément un énoncé indécidable.

Autrement dit, on n'arrive pas à décrire le comportement des nombres entiers par un système d'axiomes permettant de vérifier « mécaniquement » les preuves.

Maintenant, quelques remarques pour les puristes, que les autres pourront sauter :

• je n'ai pas précisé « au premier ordre » parce que sinon on est parti pour 10 pages de discussion sur ce qu'est une logique d'ordre supérieur
• et en quoi la théorie des ensembles n'est pas une logique d'ordre supérieur même si elle fait semblant ;
• je n'ai pas ajouté qu'en plus on peut obtenir un énoncé « vrai » car on partirait sur une discussion sur ce que c'est que le vrai ou le faux ;
• enfin je sais que ce que cet énoncé est plutôt le théorème de Gödel-Rosser, parce que le théorème de Gödel original porte non pas sur les théories non contradictoires mais sur (propriété plus forte) celles qui sont ω-consistantes.
• On peut aussi partir d'une arithmétique plus faible que Peano, par exemple Robinson.

Le codage des preuves

Une preuve, c'est une suite de caractères. Ceux qui connaissent un peu les usages informatiques ne seront pas surpris que l'on puisse coder les caractères par des nombres : par exemple, dans les encodages informatiques les plus courants, le A majuscule est codé par 65, le zéro 0 est codé par 48, etc. Ce qui est moins évident (et que je donne sans explications techniques) c'est que l'on peut coder une suite de caractères entière à l'aide d'un seul nombre, qui plus est d'une façon qui permet de raisonner et calculer sur les caractères qui la composent — par exemple, on peut écrire une formule mathématique qui dit « la suite de caractères codée par ce nombre ne contient que des A entre le centième et le millième caractères, et contient un nombre impair de caractères B ».

Mieux, pour une théorie récursivement axiomatisable, on peut écrire un énoncé mathématique qui dit « la suite de caractères codée par ce nombre est la preuve d'une contradiction dans la théorie ». On peut donc écrire finalement un énoncé arithmétique disant « il n'existe pas de nombre codant la preuve d'une contradiction dans la théorie », ce que l'on peut résumer par « il n'existe pas de contradiction dans la théorie ».

Clarifions un point. Un tel énoncé est très long, illisible pour un humain. Personne ne l'écrit, d'ailleurs : les mathématiciens prouvent une série de théorèmes du genre « on peut obtenir un énoncé qui définit telle chose », avec des choses de plus en plus complexes. Si on voulait vraiment obtenir le résultat final par écrit, il faudrait probablement utiliser un ordinateur, qui acceptera de faire sans broncher les nombreuses manipulations fastidieuses exigées. Cela n'aurait de toute façon guère d'intérêt.

Le deuxième théorème d'incomplétude

Sous les mêmes hypothèses que le premier théorème plus quelques points techniques que je ne détaillerai pas :

On trouve parmi les énoncés indécidables dans une théorie arithmétique non contradictoire un énoncé exprimant la non-contradiction de la théorie.

Rappelons que cet énoncé veut dire « il n'y a pas d'entiers codant une preuve de contradiction dans cette théorie ».

Réfléchissons maintenant à cet énoncé. S'il est faux (nous reviendrons sur la question du vrai, pour le moment prenons cet adjective dans son sens usuel sans se poser trop de questions), c'est qu'il existe une preuve de l'absurde dans la théorie arithmétique étudiée.

Mettons qu'il s'agisse de l'arithmétique de Peano… La quasi totalité des preuves que les mathématiciens font supposent, d'une façon ou d'une autre, l'arithmétique de Peano.

Autrement dit, d'une certaine façon, ils croient en l'arithmétique de Peano, et notamment croient qu'elle n'est pas contradictoire (sinon, leur travail apparaît quelque peu vain). Bref, pour la plupart des mathématiciens, il est vrai que l'arithmétique de Peano n'est pas contradictoire, autrement dit, l'énoncé dont nous parlons ci dessus est à la fois vrai et non démontrable dans l'arithmétique.

Le « meta »

Nous touchons là à un problème de fond de la compréhension des théorèmes d'incomplétude et des sujets associés.

Nous tenons des raisonnements mathématiques, et même arithmétiques, au sujet de nombres qui dénotent des textes exprimant des raisonnements dans une certaine théorie arithmétique. Autrement dit, nous avons

• d'une part la théorie mathématique (même informelle) dans laquelle nous parlons,
• et celle que nous étudions ;

=> nous devons distinguer les deux, mais parfois nous nous interrogeons sur le sens d'énoncés de la théorie étudiée lorsque nous les prenons dans leur « sens usuel » (ce qui nous donne la notion de « vérité » dont je parlais avant).

Ceci nous éclaire sur certains points de vocabulaire qui peuvent paraître mystérieux, voire mystifiants.

Dans les ouvrages spécialisés,

• on parle parfois de méta-théorie pour la théorie dans laquelle nous faisons nos raisonnements,
• pour la distinguer de la théorie étudiée.

On parle aussi de la « syntaxe » pour les énoncés de la théorie étudiée, pris sous un angle « suites de caractères respectant certaines règles d'écriture », et de « sémantique » lorsqu'on les interprète dans leur « sens usuel ».

Docteur, est-ce grave ?

L'annonce de son théorème d'incomplétude par Gödel a mis à bas le programme « formaliste » proposé par David Hilbert.

Celui-ci, bien conscient des difficultés des théories compliquées, des paradoxes toujours possibles par un choix malheureux d'axiomes, aurait en effet voulu montrer un résultat du type « il n'y a pas de contradiction possible dans la théorie des ensembles » en n'utilisant que des moyens simples, arithmétiques.

Le résultat de Gödel montre que ceci est impossible.

Toutefois, aurait-on été plus fondamentalement avancé si on avait pu prouver la non-contradiction de l'arithmétique avec les moyens de l'arithmétique ? Pardonnez une analogie : si une personne que l'on soupçonne d'être un menteur nous assure de sa plus totale honnêteté, sommes nous plus avancés ?

La plupart des mathématiciens, nous l'avons dit, rédigent des démonstrations informelles, en langue naturelle entremêlés de symboles mathématiques, avec le présupposé idéologique qu'ils pourraient, s'ils le voulaient, en tirer une preuve formelle dans la théorie des ensembles — plus précisément, dans l'axiomatique de Zermelo et Fraenkel avec l'axiome du choix, dite ZFC.

Est-ce que ce serait grave si l'on découvrait une contradiction dans ZFC ?

Pas forcément. Certains « assistants de preuve » informatisés contenaient des bugs (et, il me semble que dans certains cas, ces bugs relevaient non pas d'une erreur de programmation mais d'une erreur bien cachée dans la théorie), on a corrigé les bugs et cela n'a pas jeté à la poubelle les preuves existantes. Autrement dit, s'il y a une contradiction dans ZFC, il est plausible que l'on ne tombe pas dessus sans spécifiquement la chercher, et qu'on pourrait la corriger sans remettre en cause l'immense majorité des mathématiques existantes.

Des conclusions hasardeuses

On voit assez souvent des mentions du « théorème de Gödel » sous la plume d'intellectuels, le plus souvent issus des sciences humaines, pour justifier diverses assertions martiales, telles que :

• "Au cœur même des mathématiques, la science pourtant des certitudes, il y a de l'incertitude. Les « vérités scientifiques » sont plus plus instables et incertaines que les scientifiques le laissent entendre. (On peut compléter par quelques mentions de Kuhn et de Feyerabend.)"

• " Le « théorème de Gödel » démontre la supériorité de l'humain sur la mécanique et la technique, puisque l'humain peut savoir qu'un théorème est vrai alors que la machine n'y arrive pas."

• " Gödel « a démontré » que tout système de pensée est forcément incomplet."

Sur le premier point

je relève que les mathématiques sont sans doute la science la plus « permanente ». Même s'il y a eu au XIXe siècle un important travail d'amélioration de la rigueur et de clarification des concepts, celui-ci n'a pas remis en cause l'essentiel de ce qui avait été proposé ou démontré lors des siècles, voire des millénaires précédents. En 2015, on parle encore des axiomes d'Euclide, du théorème de Pythagore, des nombres premiers de Mersenne, des résultats d'Euler ou de Gauss… qui datent d'avant les formalisations du XIXe. Autrement dit, les résultats semblent assez « robustes » aux changements des « bases », comme si les bases formelles précisément utilisées n'étaient pas si importantes que cela.

Sur le deuxième

je pense qu'il y a une assimilation hasardeuse d'un système « mécanique », informatique, à un système de logique formelle. Ceci provient peut-être d'une idée il me semble assez dépassée de l'intelligence artificielle, où il s'agirait pour l'ordinateur de raisonner formellement sur des concepts formels, sans commettre d'erreur. Regardons autour de nous : on voit quantité de systèmes informatiques conclure sur des faits (par exemple, quand Google classe bien une page ou se rend compte qu'une image représente une scène avec un enfant et un chien) sans pour autant en avoir une justification formelle. Je ne vois pas très bien comment l'on peut conclure des théorèmes d'incomplétude de Gödel qu'il serait impossible de réaliser un système informatique qui, heuristiquement et sans rechercher une sécurité absolue du raisonnement, finirait par développer une sorte d'intuition.

Sur le troisième

rappelons que les théorèmes d'incomplétude de Gödel ne s'appliquent qu'à des systèmes formels de raisonnement logique ayant certaines caractéristiques (récursivement axiomatisables, etc.). On ne voit pas très bien comment on peut l'appliquer, comme l'on fait des auteurs aussi divers que Régis Debray ou les frères Bogdanov, aux systèmes de pensée humains ou au monde physique. Sur les systèmes de pensée, je ne m'y connais guère en philosophie mais il me semble que c'est une banalité que de dire que l'on doit bien partir de quelques « faits » que l'on admet sans pouvoir les démontrer. Par exemple, il me semble impossible de réfuter le solipsisme, le point de vue que celui qui pense est en fait seul dans l'univers et que le reste du monde n'existe que dans sa pensée ; sauf qu'il s'agit d'un point de vue remarquablement ineffectif (le monde semble vraiment se comporter comme s'il existait indépendamment de moi et il semble donc fructueux de raisonner comme si c'était le cas). Je laisse les philosophes qui me liraient développer là dessus ou m'envoyer des tomates.

Ce dont je n'ai pas parlé

On m'a demandé si je parlerais des modèles non standard de l'arithmétique. J'ai soigneusement évité de parler de théorie des modèles, tout simplement parce que ça me semble compliquer considérablement l'exposé pour les non mathématiciens (il faut parler d'ensembles etc.) et de toute façon d'introduire des confusions. Donc, non, pas d'entiers non standard, pas de modèles bizarres où il existe un objet codant la contradiction du modèle, pas de théorème de Tennenbaum.

Commentaires

---

1. Le lundi, février 9 2015, 13:43 par Typhon

« 'Dans certains cas, il est nécessaire d'admettre comme valides une infinité d'axiomes ... ce qui importe, c'est alors seulement qu'il réponde toujours par « valide » ou « invalide » au vu d'un axiome.' »

Je tique sur cette idée là : comment un programme peut-il choisir si un axiome est valide ou invalide ? Par définition, il ne peut pas démontrer leur validité en se basant sur les axiomes précédents...

Il tire à pile ou face ?

« 'un système incomplet peut être intéressant en ce qu'il exprime les points communs entre' »

Il manque la fin de cette phrase.

Typhon

2. Le lundi, février 9 2015, 14:01 par David Monniaux

@Typhon: C'est un peu technique. Dans certaines théories, il y a non seulement une liste finie d'axiomes (facile donc à reconnaître par un programme) mais aussi des « schémas d'axiomes », par exemple celui de récurrence dans l'arithmétique de Peano : un ensemble infini, mais régulier, d'axiomes (pour la récurrence : c'est parce qu'on a le droit de la faire sur n'importe quelle propriété, donc il y a un axiome instance du schéma par propriété). Le programme doit alors tester si l'axiome a la forme prévue par le schéma.

3. Le lundi, février 9 2015, 14:26 par Subbak

@Typhon: Ce dont David n'a pas vraiment parlé (pourquoi d'ailleurs ? Je ne suis pas logicien, donc peut-être que la complexité de ce que je vais dire m'échappe...) c'est qu'il existe un systéme d'axiome complet, cohérent et qui décrit Peano : on part de Peano, on prend le premier énoncé (celui de plus petit texte) indécidable, on le rajoute comme axiome, et ainsi de suite.

Le problème avec ce système est qu'il n'est pas possible pour un calculateur formel de savoir ce qui est un axiome, vu que ça nécessite de savoir ce qui est indécidable dans l'arithmétique de Peano. Donc ce système n'est pas récursivement axiomatisable.

4. Le lundi, février 9 2015, 14:48 par David Monniaux

@Subbak: David Madore connaît mieux que moi les subtilités de ce genre de constructions. Dans mes souvenirs, on se retrouve à rajouter une infinité d'axiomes indexés par les ordinaux (Peano=0, Peano+consistance de Peano=1, etc. et puis on en a ⍵ et on continue de compléter et on en a 2⍵ puis ⍵²...) jusqu'à ce que l'on arrive sur un ordinal où le système n'est plus récursivement axiomatisable. C'est effroyablement technique par rapport au niveau de mon article.

On peut aussi prendre comme axiomes l'ensemble des théorèmes vrais sur les entiers ; autrement dit importer l'ensemble de ce que dit la méta-théorie au sujet des entiers dans la théorie. C'est un système complet mais non récursivement axiomatisable. En parler aurait je crois risqué d'induire le lecteur en confusion...

5. Le mardi, février 10 2015, 00:21 par Subbak

Le premier paragraphe donne clairement trop de détails pour cet article.

Mais le second ne me paraît pas excessivement compliqué, après effectivement c'est possible que ça crée de la confusion, mais je trouve que c'est un peu dommage de ne pas avoir un peu plus explicité la nécessité de l'hypothèse "récursivement axiomatisable".

6. Le mardi, février 10 2015, 10:50 par Mouton

J'ai proposé ce texte à mes étudiants comme vulgarisation des théorèmes de Gödel. Merci :)

7. Le mercredi, février 11 2015, 16:05 par Frank Wolff

Vous dites : « Un systèmes d'axiomes contradictoire n'a aucun intérêt parce qu'avec lui tout est démontrable »

Ergo, dans un système d’axiomes contradictoire, tout est démontrable, rien n’est indécidable, il est donc complet :

(Contradictoire => complet)

Le premier théorème dit : « Une théorie récursivement axiomatisable, non contradictoire, et capable de représenter l'arithmétique de Peano, est forcément incomplète : elle contient forcément un énoncé indécidable »

Soit (Non contradictoire => incomplet)

En déduit-on que : pour une théorie récursivement axiomatisable capable de représenter l'arithmétique de Peano,

(contradictoire < = > complet)

ou suis-je victime de confusion simplificatrice ?

8. Le mercredi, février 11 2015, 16:51 par Fank Wolff

Par ailleurs, si je comprends bien le commentaire 4 de David, à partir du second théorème je peux :

Soit ajouter quelque chose comme un axiome autoproclamant la contradiction de la théorie, aboutissant à une théorie incontestablement contradictoire à laquelle ne s’appliquent plus les 2 théorèmes.

Soit ajouter quelque chose comme un axiome autoproclamant la non contradiction de la théorie, conservant l’applicabilité des deux théorèmes. On peut recommencer aussi longtemps que l’on conserve la récursivité, qui finit par se perdre dans des ordinaux mystérieux. Mais dans le même temps, on gagne la complétude et la non contradiction (ipso facto toutes deux prouvables par le système, pour reprendre la métaphore du Menteur, « bonjour la confiance », mais est-ce également prouvable au niveau « méta » ?).

Finalement, le second théorème donne une nature d’énoncé indécidable pour une « classe » de théories, portant en eux un soupçon d’autoréférentialité. Mais ce même commentaire 4 de David indique qu’il y a d’autres natures d’énoncés indécidables pour ces mêmes théories, qui ont trait à ce qui est « vrai » sur les entiers. Importer ces énoncés aboutit aussi à un système non récursivement axiomatisable, mais complet et non contradictoire.

(Subbak prend des énoncés indécidables dont il sait qu’ils existent, mais ne leur donne pas la parole : ce sont peut-être déjà ceux de David Madore, ou Monniaux !).

Là, j’ai au moins deux questions :

1. Qu’est-ce qui est « vrai » sur les entiers sans être un théorème de Peano ?

2. Les deux constructions mènent-elles au « même » système. S’agissant de systèmes formels, déjà, définit-on des « isomorphismes » entre systèmes ?

Sur le solipsisme, Borges a dit de Berkeley (en fait, écrit) que ses arguments étaient irréfutables, mais qu’ils n’emportaient aucune conviction. Curieux comme, encore une fois, rôde la crainte du Menteur…

9. Le dimanche, février 15 2015, 08:36 par David Monniaux

@Frank: Est vraie sur les entiers une formule exprimant qu'il n'existe aucun codage de Gödel d'une preuve de l'absurde dans l'arithmétique de Peano alors qu'on ne peut la démontrer dans ladite arithmétique.

10. Le dimanche, février 15 2015, 13:19 par telchar

@Frank: « Soit ajouter quelque chose comme un axiome autoproclamant la contradiction de la théorie, aboutissant à une théorie incontestablement contradictoire à laquelle ne s’appliquent plus les 2 théorèmes. »

Si on appelle PA l'arithmétique de Peano et Con(PA) la proposition énonçant la non-contradiction (consistance) d'icelle, alors la théorie PA+non(Con(PA)) est non contradictoire, sous réserve que PA le soit.

Cela peut paraître un peu surprenant. Bien que non contradictoire, cette théorie a des côtés très insatisfaisants : par exemple elle démontre (à tort) qu'une certaine machine de Turing qui ne s'arrête pas s'arrête. Mais il est impossible d'en déduire une contradiction qui s'écrirait en un nombre fini d'étapes : pour voir l'erreur de la théorie il faudrait faire tourner ladite machine de Turing jusqu'à la fin des temps.

De même, elle démontre à tort que PA est contradictoire, mais elle est incapable d'écrire une "vraie" démonstration qui nous convaincrait que PA est vraiment inconsistante.

Enfin, Con(PA+non(Con(PA))) est indécidable dans PA+non(Con(PA)).

En résumé on peut bien ajouter à la théorie un axiome énonçant sa propre contradiction, on obtient une théorie non contradictoire et les théorème s'y appliquent encore.

(En espérant ne pas m'être mélangé les pinceaux dans ces considérations glissantes mais passionnantes)

11. Le lundi, février 16 2015, 18:10 par SB

« Le programme de vérification des preuves va prendre chaque axiome et vérifier s'il est valide »

Je n'ai pas compris quelle était la définition de « valide », apparemment la question est abordée dans les commentaires 1 et 2, mais il faudrait peut-être expliciter cette définition dans le corps du texte ?

12. Le mardi, février 17 2015, 14:19 par Xavier Combelle

Bravo et merci, c'est nettement plus satisfaisant que l'interview des frères Bogdanoff

13. Le mercredi, avril 29 2015, 19:11 par François

Le Professeur Rollin, sur le théorème de Gödel. Et Régis Debray.

http://rf.proxycast.org/10215856965...