29 mai 2024 ∙ Retour à l'accueil du blog
Quand j'étais en terminale, notre professeure de philosophie a voulu faire venir un collègue de maths pour nous présenter le théorème d'incomplétude de Gödel, mais l'idée ne s'est finalement pas réalisée. Cinq ans plus tard, j'ai voulu combler ma déception de l'époque en écrivant une « toute petite » note de vulgarisation sur le sujet, complément à une entrée technique précédente. Sauf que cette note a enflé bien au-delà du raisonnable, même si j'ai renoncé à présenter aussi le deuxième théorème d'incomplétude. Je la publie malgré tout, en espérant qu'elle serve à quelqu'un.
Le premier théorème d'incomplétude de Gödel dit, de façon approximative et résumée, qu'il existe des énoncés mathématiques ni démontrables ni réfutables. C'est l'un des plus célèbres et étonnants de toutes les mathématiques, et on trouve bien sûr des milliers d'articles ou vidéos de vulgarisation existants à son sujet. Malheureusement, c'est un sujet extrêmement glissant, sur lequel il est très facile de dire des bêtises (donc non seulement le vulgarisateur doit éviter de dire des bêtises, mais il doit aussi anticiper les bêtises que va probablement croire le public). Je vais donc donner plus de détails que la plupart, en espérant que le résultat ne soit pas trop technique (n'hésitez pas à poser toute question dans les commentaires). Je crois que c'est le prix à payer pour comprendre vraiment la subtilité du théorème. Voir tout de même cette vidéo d'un vulgarisateur populaire pour des explications très accessibles et pas trop fausses.
Il se trouve aussi que ce théorème est très relié à l'informatique théorique, mon domaine d'études, et je vais le prouver par un chemin qui n'est pas le plus court ni le plus habituel, mais qui fait mieux ressortir le côté informatique. Et puisque j'ai moi-même mis trois ans après le bac avant de réaliser que l'informatique pouvait être un domaine scientifique passionnant et pas seulement une technique, j'en ai profité pour en donner un aperçu… incomplet, bien sûr.
« L'informatique n'est pas davantage la science des ordinateurs que l'astronomie n'est la science des télescopes. » — citation probablement apocryphe de Dijkstra
L'informatique ne se réduit pas à la programmation — et encore moins à l'utilisation de logiciels ou à la réparation d'ordinateurs — mais est également une branche de la science, largement reconnue depuis quelques dizaines d'années, et toujours en plein essor. Pour désigner les aspects plus abstraits de l'informatique, on emploie souvent les termes « informatique théorique » ou « informatique fondamentale ». Les frontières restent cependant très floues entre l'informatique théorique et la programmation d'une part, entre l'informatique théorique et les mathématiques d'autre part, au point que l'informatique théorique est parfois classée purement et simplement dans les mathématiques.
Pour donner une idée des questions que se pose l'informatique théorique, citons quelques sous-domaines :
L'algorithmique vise à trouver des algorithmes efficaces pour toutes sortes de problèmes, par exemple trouver toutes les occurrences d'un mot dans un texte, trier une liste de nombres, calculer le contour géométrique (enveloppe convexe) d'un ensemble de points, calculer le nombre minimal de caractères à ajouter/supprimer/modifier pour transformer un mot en un autre, etc.
La complexité pourrait ressembler à première vue à l'algorithmique car elle cherche aussi à caractériser le degré de difficulté d'un problème algorithmique. Pourtant, ses méthodes sont assez différentes. Pour faire simple, un algorithmicien (sous-entendu : ou une algorithmicienne) cherche toujours à rogner pour trouver l'algorithme le plus optimal possible, alors qu'un théoricien de la complexité est satisfait dès qu'il obtient un algorithme seulement « assez efficace ». À l'inverse, la complexité s'intéresse beaucoup aux manières de prouver qu'un problème est difficile, qu'il ne peut pas être résolu efficacement, ainsi qu'à la difficulté relative des problèmes : prouver qu'un certain problème est plus difficile qu'un autre. Cette étude conduit à ranger les problèmes dans des « classes de complexité », dont il existe des centaines (on peut se faire une petite idée en visitant le site complexityzoo.net), et entre lesquelles on tente de comprendre les liens.
L'une des classes fondamentales est la classe P des problèmes que l'on peut « facilement » résoudre (en un certain sens précis). Une autre est la classe NP des problèmes dont on peut « facilement » vérifier une solution si on la devine. Intuitivement, il semble que pouvoir vérifier une solution n'aide pas forcément à trouver la solution, donc on peut penser qu'il existe des problèmes NP qui ne sont pas P, et on connaît un nombre faramineux de problèmes dont on soupçonne fortement que c'est le cas (pour donner un exemple simple, le problème subset sum : étant donnée une liste de nombres entiers et un entier n, peut-on retirer certains éléments de la liste de sorte que la somme des nombres restants fasse n ?). Pourtant, cette question « P = NP » reste ouverte. C'est de très loin la question ouverte la plus célèbre et importante de l'informatique (elle fait aussi partie des problèmes du millénaire dotés d'un prix d'un million de dollars par l'institut Clay).
La théorie des graphes a pour objet d'étude les graphes, qui sont des ensembles de points appelés sommets, et d'arêtes qui relient les sommets. Dans un graphe, on ne s'intéresse pas à la position géométrique des points, seulement à la structure du réseau. On peut penser au graphe d'un réseau de transports, au graphe dont les sommets sont les élèves d'une classe avec une arête entre deux amis, etc.
La cryptographie développe des algorithmes pour communiquer de manière secrète, pour vérifier qu'un message provient d'une personne donnée, etc. Nous utilisons ce genre d'algorithmes tous les jours, dès que nous nous connectons à une page Web en « https:// ».
La sémantique a pour but de définir formellement le comportement d'un langage de programmation — ce qui n'est absolument pas évident, par exemple lorsque le programme exécute plusieurs tâches à la fois sur plusieurs processeurs.
La théorie des automates s'intéresse aux automates, qui dans ce contexte ne sont pas des robots, mais des machines abstraites dont la quantité de mémoire est fixée à l'avance. Il existe énormément de types d'automates, et ils servent entre autres à lire la syntaxe des langages de programmation.
La vérification est plus souvent associée à la pratique et à l'industrie que les domaines précédents. Elle a pour but de s'assurer de l'absence de bugs dans les programmes, ceci à l'aide d'un éventail de méthodes dont certaines sont très liées aux automates, d'autres à la logique et à la sémantique.
et enfin, deux domaines qui nous intéressent ici :
La calculabilité explore les limites théoriques du calcul. Elle cherche à distinguer les problèmes qui peuvent être résolus algorithmiquement de ceux qui ne le peuvent pas.
La logique, dans la zone grise entre mathématiques et informatique, s'intéresse aux systèmes de déduction formels, ainsi qu'à leurs interprétations mathématiques (appelées modèles). Précisons un peu ceci.
En première approche, on pourrait dire que la logique est la science du raisonnement. Elle étudie des systèmes formels qui permettent de construire des propositions, également appelées les énoncés logiques, et des démonstrations qui établissent la validité de certaines propositions. Chacun de ces systèmes est appelé une logique.
L'histoire de la logique est longue et tortueuse. Le premier livre qui s'apparente aux mathématiques telles qu'elles sont pratiquées aujourd'hui est probablement les Éléments du penseur grec Euclide, un traité de géométrie qui remonte au IIIè siècle avant notre ère, à l'influence phénoménale sur l'enseignement des mathématiques jusqu'au XIXè siècle. Euclide part d'un petit nombre de postulats, des vérités acceptées comme vraies sans démonstration, et prouve tous ses théorèmes en montrant comment ils se déduisent logiquement des postulats. C'est là le principe des mathématiques aujourd'hui : les mathématiciens prouvent des théorèmes par des démonstrations formelles, qui se veulent incontestables, et ces démonstrations reposent sur quelques postulats, appelés de manière plus moderne les axiomes.
Néanmoins, si Euclide avait déjà formalisé ses postulats, il a fallu attendre la fin du XIXè siècle pour que les règles de la déduction logique elle-même commencent à être formalisées. L'une des tentatives les plus marquantes fut les Principa Mathematica, ouvrage de Russell et Whitehead publié entre 1910 et 1913, qui résout certains paradoxes identifiés dans les théories antérieures. (Je recommande au passage la bande dessinée Logicomix, qui narre l'histoire de Russell et de ce livre.) Le système passablement alambiqué des Principa Mathematica a été largement simplifié, et les mathématiques se font maintenant conventionnellement dans la théorie des ensembles de Zermelo-Fraenkel avec l'axiome du choix, abrégée en ZFC, progressivement peaufinée par Zermelo, Fraenkel et Skolem entre les années 1900 à 1920. Cette théorie donne seulement les axiomes, elle s'appuie sur un langage logique dit du premier ordre. Un grand progrès fut accompli par Gentzen en 1934 avec l'invention de la déduction naturelle, un système de déduction assez simple pour la logique du premier ordre. Au même moment, Church, Turing, Gödel, Kleene, entre autres, ont posé les fondements de l'informatique en définissant la notion d'algorithme, et étudié les liens avec la logique, ce qui a conduit en particulier au théorème d'incomplétude de Gödel.
Beaucoup des logiques modernes, dont ZFC, suivent donc une structure de tour à trois étages :
Le langage : Il définit la forme des propositions logiques. Par analogie avec la langue française, le langage est la grammaire de la logique. Le langage ne se préoccupe pas de vérité. De même que la phrase « La Terre est plate. » est grammaticalement correcte, bien que fausse, la suite de symboles « 2 + 2 = 5 » est une proposition bien formée du langage des mathématiques usuelles.
Le système de déduction : Il donne les règles utilisées pour former les démonstrations. Par exemple, une certaine règle de la déduction naturelle affirme intuitivement que si on peut prouver A, et par ailleurs on peut prouver B, alors on peut combiner les deux pour former une preuve de « A et B ».
La théorie : Puisqu'il faut bien partir quelque part, on adopte comme axiomes des propositions admises sans démonstration, à partir desquelles on peut prouver d'autres propositions. Ces axiomes forment une « théorie ».
Un théorème est une proposition qui peut être prouvée en suivant les règles de déduction à partir des axiomes. Le but est que tous les théorèmes soient incontestablement vrais, et pour cela, il faut que les règles de déduction soient raisonnables, et que les axiomes de départ soient vrais. Toutes les mathématiques reposent donc sur la croyance que les axiomes de ZFC sont vrais. On aimerait que les axiomes soient tellement évidents qu'ils sautent aux yeux de toute personne sensée. Malheureusement, pour ZFC, ce n'est pas tout à fait aussi simple.
La standardisation de ZFC comme fondement des mathématiques n'a pas empêché l'étude de quantités d'autres systèmes logiques, dont certains sont pris comme fondements alternatifs possibles pour les mathématiques, et d'autres n'ont pas cet objectif mais sont intéressants pour des raisons différentes. On croisera plusieurs théories alternatives dans la suite, mais voici aussi quelques systèmes de déduction alternatifs :
La théorie des types, qui fait un pont étonnant entre la logique et les langages de programmation, et s'en sert pour créer des systèmes logiques où les preuves sont en fait des programmes. (Pour les très curieux, chercher « interprétation de Brouwer-Heyting-Kolmogorov » ou « correspondance de Curry-Howard ».)
La logique intuitionniste ou constructive : Pour l'expliquer intuitivement, imaginons qu'une certaine semaine, il a plu le lundi, et il a fait beau le dimanche suivant. En logique classique, on peut prouver le théorème : « un certain jour de la semaine, il a fait beau alors que le lendemain, il a plu ». En effet, il faut bien qu'un jour de soleil soit suivi d'un jour de mauvais temps pour que la semaine commence par du beau temps et finisse par du mauvais temps. On ne sait pas de quel jour on parle, on sait simplement qu'il existe. En logique intuitionniste, ce type de raisonnement est rejeté : on accepte une preuve qu'un objet existe seulement si elle est capable de montrer l'objet en question.
L'une des applications les plus spectaculaires de la logique est le développement des assistants de preuve, qui sont des sortes de langage de programmation où au lieu d'encoder des programmes, on encode des preuves logiques (en fait, ils sont souvent fondés sur la théorie des types et mélangent donc les deux). Parmi les plus plus utilisés, on peut citer Lean, Coq, Agda et Isabelle. Les assistants de preuve servent à vérifier les démonstrations, ce qui libère largement du risque d'erreur humaine qui est toujours présent, surtout dans des démonstrations de plusieurs centaines de pages. Ils ont connu de grands succès, par exemple la formalisation en Coq du théorème de Feit-Thompson, un grand théorème des mathématiques du XXè siècle, dont la démonstration sur papier fait environ 250 pages. On peut aussi penser à CompCert, un compilateur pour le langage de programmation C, écrit en Coq, qui s'accompagne d'une preuve (aussi en Coq) que le compilateur implémente bien la norme qui définit le langage C.
Pour rendre les choses plus concrètes, voici un petit exemple d'utilisation de Coq où je prouve un théorème très simple : si P et Q, alors Q et P. À gauche, on voit les commandes que je tape, et à droite, un écran en deux parties qui évolue au fur et à mesure de la démonstration : en-dessous de la barre horizontale =======, ce qu'il reste à prouver, et au-dessus, ce que l'on peut utiliser pour le prouver.
La plupart des assistants de preuve sont capables de démonstration automatique, c'est-à-dire qu'ils peuvent non seulement vérifier des preuves, mais aussi trouver eux-mêmes des preuves. Par exemple, le théorème prouvé dans la vidéo ci-dessus peut aussi se prouver en une seule commande Coq, « tauto. ». Dans ce domaine, on reste toutefois très loin du niveau des humains. À l'heure actuelle, la démonstration automatique est suffisamment développée pour décharger les humains de détails simples mais fastidieux dans les preuves, mais n'est pas capable de proposer des preuves réellement originales.
De manière plus générale, la logique occupe une place centrale en informatique, ayant des liens avec presque tous les autres sous-domaines, même les plus inattendus. Par exemple, aussi surprenant que cela puisse paraître, il existe un lien profond entre complexité et logique, la complexité descriptive, qui est un ensemble de théorèmes du type de « Les problèmes de [une certaine classe de complexité] sont exactement les problèmes qui peuvent être formulés dans [une certaine logique] ». Cette correspondance est fascinante puisqu'elle réduit que des questions sur l'efficacité des algorithmes, comme « Est-ce que P = NP ? », à des questions purement logiques de la forme « Est-ce que telle logique est équivalente à telle autre ? », et c'est l'une des pistes pour résoudre la fameuse question P = NP à un million de dollars. (Pour les très curieux qui connaissent déjà de l'informatique théorique, chercher aussi « théorème de Courcelle » pour un pont avec la théorie des graphes et « théorème de Büchi-Eglot-Trakhtenbrot » pour la théorie des automates.)
Cette longue introduction à la logique terminée, en route vers le théorème de Gödel ! La première étape passe par un peu de calculabilité.
Comme expliqué plus haut, la théorie de la calculabilité cherche à distinguer les problèmes que l'on peut ou que l'on ne peut pas résoudre à l'aide d'un algorithme. Pour cette étude théorique, on raisonne sur des machines idéalisées, qui disposent d'une mémoire illimitée et peuvent calculer pendant un temps illimité. Lorsque l'on détermine qu'un problème est algorithmiquement réalisable en théorie, l'histoire n'est pas vraiment terminée, car il est possible, par exemple, qu'il demande un temps de calcul de plusieurs milliards d'années sur un ordinateur réel. Il faut alors étudier le degré d'efficacité avec lequel on peut le résoudre — mais ceci sort du domaine de la calculabilité pour rentrer dans la complexité. En revanche, si un problème est algorithmiquement insoluble même avec un temps de calcul et un espace mémoire illimités, on ne peut évidemment pas espérer le résoudre dans la vraie vie.
Pour raisonner sur les algorithmes, il faut d'abord disposer d'une définition précise d'un algorithme, ce qu'on appelle un modèle de calcul. Or, il existe des milliers de langages de programmation différents, et dans le domaine théorique, des centaines de modèles de calcul ont également été inventés et étudiés. On peut donc s'interroger : la calculabilité dépend-elle du langage de programmation choisi ? Est-ce que ces langages se distinguent seulement par l'efficacité avec laquelle ils s'exécutent et la facilité à les programmer, ou est-ce qu'ils sont fondamentalement différents au sens où certains problèmes seraient solubles dans un langage et pas dans un autre ?
Historiquement, le tout premier modèle de calcul a été inventé non pas par Turing, contrairement à une croyance répandue, mais par Gödel et Herbrand, et s'appelle les « fonctions générales récursives ». Ce sont des fonctions mathématiques, qui prennent un entier et renvoient un entier, et elles se définissent en combinant quelques fonctions de base par des opérations comme « répéter n fois ».
Quelques années plus tard, Church a deuxième modèle de calcul, appelé le λ-calcul (lire lambda-calcul). Je ne vais pas l'expliquer ici car il est relativement abstrait et peu intuitif. Disons simplement, pour faire très court, qu'en λ-calcul, on peut faire des calculs comme (λ x ⋅ y x) (λ z ⋅ z z) = y (λ z ⋅ z z), où la notation « λ x ⋅ … » représente une sorte de fonction qui prend un argument x et renvoie l'expression dans les points de suspension, et l'expression (λ x ⋅ …) T peut se simplifier en remplaçant x par T dans ces points de suspension.
Peu après, Turing a inventé un nouveau modèle de calcul, les machines de Turing, qui préfigure le fonctionnement réel d'un ordinateur actuel. Une machine de Turing est un programme qui s'exécute sur une bande de travail, un ruban infini dont chaque case peut contenir 0 ou 1. Sur le ruban se déplace une tête de lecture. Les instructions possibles dans le programme sont de trois types :
Au début du calcul, on place une suite de 0 et de 1 sur la bande, qui est l'entrée du programme. On laisse la machine s'exécuter, et si le programme termine, il laisse sa sortie écrite sur la bande.
Ces trois modèles de calcul semblent a priori très éloignés. L'un part d'une intuition mathématique abstraite, les fonctions sur les entiers, le deuxième d'une intuition mathématique encore plus abstraite, le remplacement d'une variable par une expression, et le troisième d'une intuition plus physique et concrète, une machine qui exécute des étapes de calcul sur une bande de mémoire. Pourtant, les travaux de Church, Kleene, Rosser et Turing ont montré que tous ces modèles de calcul sont en fait équivalents, au sens où ce qui est calculable par une fonction générale récursive est exactement ce qui est calculable en λ-calcul, et aussi ce qui est calculable par une machine de Turing.
Les informaticiens s'intéressent aujourd'hui à de nombreux autres modèles de calcul, comme les grammaires, les systèmes de réécritures, les machines à compteurs, les calculs à combinateurs, les machines à accès randomisé, etc. À chaque fois, il a pu être prouvé que ces modèles étaient équivalents aux existants. C'est aussi le cas du jeu d'instructions d'un ordinateur, et de tous les langages de programmation usuels (on dit qu'ils sont Turing-complets). De plus, Turing a proposé une analyse du processus de calcul par un humain, en supposant qu'il se fait par des étapes prédéterminées dans un programme fini sur une mémoire finie, et montré que tout calcul de ce type peut être réalisé par une machine de Turing. Ceci conduit à penser que tous ces modèles de calcul équivalents définissent exactement ce qui est calculable dans le monde physique, par un humain ou un ordinateur, et cette hypothèse est appelée thèse de Church-Turing (ou simplement thèse de Church). On ne peut pas la prouver formellement — de même qu'on ne peut pas prouver une loi physique, seulement l'observer — mais elle repose néanmoins sur des bases solides.
On dit qu'un problème est décidable s'il peut être résolu par une machine de Turing, ou un programme dans n'importe lequel des autres modèles de calcul équivalents. Sinon, il est indécidable. L'un des apports fondamentaux de Turing fut donner un problème indécidable simple. C'est le problème de l'arrêt, qui consiste à déterminer si une machine de Turing donnée, sur une entrée donnée, va finir par s'arrêter et donner le résultat du calcul, ou bien va continuer son calcul éternellement.
Imaginons qu'il existe un programme ARRÊT qui résout le problème de l'arrêt. On construit un programme FOU qui prend en entrée le code d'un programme, CODE.
Pour le dire en d'autres mots, FOU(CODE) termine exactement quand CODE(CODE) ne termine pas.
Vous ne voyez pas le problème ? Que se passe-t-il si on exécute FOU(FOU) ? On voit que FOU(FOU) termine exactement si FOU(FOU) ne termine pas… c'est contradictoire ! Donc l'algorithme ARRÊT ne pouvait pas exister. CQFD.
Pour donner un point de vue légèrement différent sur cette preuve, on propose traditionnellement le défi d'écrire, dans son langage de programmation préféré, un programme qui, lorsqu'on l'exécute, affiche son propre code source. Un tel programme s'appelle une quine (du nom du logicien Willard Van Orman Quine). Vous pouvez essayer de vous inspirer de la preuve pour écrire une quine en Python par exemple (ce n'est pas évident du tout). Cette technique à base de programmes qui s'appellent sur leur propre code source permet en fait à n'importe quel programme d'obtenir accès à son propre code source. Ce résultat est appelé théorème de récursion de Kleene. Voici la preuve reformulée avec ce théorème, qui est peut-être plus compréhensible :
Imaginons qu'un programme ARRÊT soit capable de résoudre le problème de l'arrêt. On construit un programme FOU. Ce programme utilise le théorème de récursion de Kleene pour obtenir son propre code source, et il exécute ARRÊT(FOU) pour savoir si ARRÊT « pense » qu'il va terminer. Il utilise ce résultat pour « contredire » ARRÊT, en bouclant si ARRÊT dit qu'il doit terminer, et en s'arrêtant si ARRÊT dit qu'il doit boucler. On a une contradiction, donc ARRÊT ne peut pas exister.
Il existe même un théorème très général, le théorème de Rice, d'après lequel toutes les questions sur les programmes sont indécidables dès lors qu'elles ne dépendent que du comportement du programme, et pas de la manière dont il est écrit (sauf deux cas particuliers, quand la réponse est toujours oui, ou bien toujours non). Par exemple, il n'existe pas d'algorithme pour décider si un programme ne plante jamais, ou si un programme Python est une réponse correcte à la question 4b du bac de maths de l'année XYZ.
En 1928, suite au mouvement de formalisation de la logique et d'éclaircissement des fondements des mathématiques, Hilbert s'est demandé s'il pouvait exister un algorithme qui prenne en entrée une proposition logique, et qui détermine si la proposition est prouvable dans une théorie donnée. La question est devenue connue sous le nom allemand « Entscheidungsproblem », soit « problème de la décision ». Elle était délicate au départ, car on pouvait prouver qu'un algorithme existait pour un problème en écrivant simplement l'algorithme, mais pour prouver qu'un algorithme ne pouvait pas exister, il fallait d'abord une définition précise d'un algorithme, et cette définition n'a été trouvée que dans les années 1930 avec la thèse de Church-Turing.
Plusieurs théories intéressaient les logiciens. Il y a ZFC, bien sûr, mais aussi une certaine théorie beaucoup plus simple appelée arithmétique de Peano. La théorie ZFC est extrêmement générale et parle d'objets appelés ensembles qui sont des collections d'autres objets (qui dans ZFC sont en fait à leur tour des ensembles, etc.). Cette notion d'ensemble est difficile à cerner et sujette à débats. L'arithmétique de Peano est bien plus restreinte et parle simplement des entiers naturels (c'est-à-dire les nombres entiers positifs : 0, 1, 2, 3, 4, …). Elle comporte huit axiomes, dont les sept premiers sont complètement évidents (il y a par exemple 0 + x = x et 0 × x = 0), et le huitième (subtilité : c'est en fait un ensemble d'axiomes) est le principe de récurrence, que je n'expliquerai pas ici car il est un peu moins évident (il est enseigné en spécialité maths en terminale), mais sur lequel il n'y a aucun doute.
Tarski pensait qu'il était possible de résoudre algorithmiquement l'Entscheidungsproblem pour l'arithmétique de Peano. Il pensait même que la question serait assez facile. Il l'a confiée à un étudiant, Presburger, qui a réussi à trouver un algorithme pour une version affaiblie de l'arithmétique de Peano, où on enlève la multiplication, mais qui a bloqué sur la multiplication.
Ce sont Church et Turing qui ont fini par trancher indépendamment la question, en montrant que l'Entscheidungsproblem pour l'arithmétique de Peano (avec la multiplication) est en fait indécidable. Voici l'approche de Turing. Il avait prouvé que le problème de l'arrêt est indécidable. Il a montré qu'étant donnée une machine de Turing et une entrée, la question « Est-ce que cette machine de Turing s'arrête si on l'exécute sur cette entrée ? » peut être formulée dans l'arithmétique de Peano, via un encodage qui est très fastidieux à expliciter complètement mais ne présente pas de vraie difficulté (voir par exemple ici pour une démonstration avec tous les détails).
Imaginons qu'il existe un algorithme PROUVABLE-PEANO qui prend une proposition de l'arithmétique de Peano et renvoie oui si elle est prouvable, et non sinon. Alors on pourrait construire l'algorithme qui prend une machine de Turing et une entrée, qui traduit la question « Est-ce que cette machine s'arrête sur cette entrée ? » dans l'arithmétique de Peano, et qui utilise PROUVABLE-PEANO pour déterminer si cette proposition est prouvable.
L'observation-clé est que si la machine s'arrête, alors l'arithmétique de Peano peut le prouver, parce que la proposition « la machine s'arrête » dit qu'il existe une suite finie d'étapes qui représente le calcul, et on peut produire une démonstration qui dit « Voici la suite d'étapes, et je vérifie que les règles de calcul des machines de Turing ont bien été respectées ». Donc, si la machine s'arrête, PROUVABLE-PEANO va répondre oui. Inversement, si la machine ne s'arrête pas, PROUVABLE-PEANO ne peut que répondre non, car l'arithmétique de Peano ne peut que prouver des choses vraies — on le sait car tous ses axiomes sont suffisamment évidents. Ainsi, le résultat renvoyé par PROUVABLE-PEANO résout la question de l'arrêt. On a donc un algorithme qui résout le problème de l'arrêt. Mais ce n'est pas possible, puisque le problème de l'arrêt est indécidable ! C'est donc que l'algorithme PROUVABLE-PEANO ne pouvait pas exister. CQFD !
Dans sa nouvelle La Bibliothèque de Babel, l'écrivain Jorge Luis Borges imagine une immense bibliothèque qui contient tous les livres de 410 pages possibles. On trouve donc, dans cette bibliothèque, les 410 premières pages des Misérables, et aussi les 410 pages suivantes, mais également les pages 200 à 609 du tome 7 de Harry Potter, les 410 premières pages de La République de Platon avec une faute d'orthographe à la page 306, les pages 150 à 249 du code civil français suivies des pages 324 à 633 des archives de la ville de Caen au XIXè siècle, et des zillions de suites de symboles qui n'ont aucun sens.
Si cette métaphore m'intéresse, c'est parce que parmi tous ces livres doivent aussi se trouver des démonstrations mathématiques. On y retrouverait par exemple les 410 premières pages des Éléments d'Euclide, ou des Principia Mathematica. Mais on trouverait aussi des textes avec des démonstrations fausses.
Étendons l'expérience de pensée et imaginons que nous ayons accès à une bibliothèque infinie où se trouvent tous les livres qui peuvent exister (par exemple avec un premier rayon pour les livres d'une seule page, un deuxième pour les livres de deux pages, et ainsi de suite). Si nous avions en plus une vie éternelle pour explorer cette bibliothèque, nous pourrions chercher à résoudre un problème ouvert, par exemple P = NP, non pas en y réfléchissant nous-mêmes, mais en lisant un par un les livres de cette bibliothèque jusqu'à trouver une démonstration qui résolve notre problème.
Le point essentiel est qu'il faut de la créativité pour imaginer une démonstration, mais il n'en faut aucune pour vérifier une démonstration, pourvu qu'elle soit rédigée de manière suffisamment formelle. Il suffit de regarder si la démonstration part bien des axiomes et si les règles de la logique sont bien suivies à chaque étape.
D'ailleurs, nous venons de parler d'algorithmes pour décider si une proposition est prouvable. N'avons-nous pas là un algorithme ? Supposons que nous voulons savoir si une certaine proposition P, disons de l'arithmétique de Peano, est vraie ou fausse. Nous pouvons parcourir virtuellement la bibliothèque, en commençant par les suites de 1, 2, 3, 4 symboles, et ainsi de suites, pour rechercher une démonstration de P, ou une démonstration que P est fausse. (Si nous trouvons une démonstration que P est fausse, alors en particulier P n'est pas prouvable, car l'arithmétique de Peano ne prouve que des propositions vraies.) Au bout d'un moment, nous finirons par trouver la démonstration, donc nous saurons si P est prouvable ou pas. Ainsi nous aurons résolu l'Entscheidungsproblem. Pourtant, nous venions de voir que c'était impossible ! Où est la faille ?
Elle réside tout simplement dans la croyance que nous allons trouver une démonstration que P est vraie ou une démonstration que P est fausse. Le raisonnement que nous venons de faire prouve qu'une telle démonstration n'existe pas toujours, sans quoi l'Entscheidungsproblem serait décidable. Nous sommes enfin arrivés au premier théorème d'incomplétude ! Nous avons prouvé qu'il existe dans l'arithmétique de Peano des propositions dont l'arithmétique de Peano ne prouve ni qu'elles sont vraies ni qu'elles sont fausses. On dit que l'arithmétique de Peano est incomplète.
Résumons tout le chemin parcouru pour y arriver :
J'ai énoncé le théorème pour l'arithmétique de Peano ici, mais on peut refaire le cheminement pour d'autres théories, comme ZFC. Voici les ingrédients dont on a besoin :
Pour pouvoir vérifier les preuves, il faut que la théorie soit décidablement axiomatisée, c'est-à-dire qu'il doit exister un algorithme qui vérifie si une proposition est un axiome de la théorie.
Pour pouvoir traduire « cette machine de Turing termine sur cette entrée » dans la théorie, il faut que la théorie soit au moins aussi puissante que l'arithmétique de Peano.
Enfin, pour que la prouvabilité de cette proposition résolve le problème de l'arrêt, il faut que la théorie ne prouve que des choses justes, au moins pour ce qui relève de l'arithmétique. Toutefois, même si je ne vais pas donner les détails, il se trouve qu'on peut modifier la preuve pour supposer seulement que la théorie est cohérente, c'est-à-dire qu'elle ne se contredit pas elle-même, qu'elle ne prouve pas un énoncé et son contraire. (Depuis que ChatGPT existe, j'espère qu'il est clair qu'on peut être cohérent avec soi-même tout en disant des choses parfaitement fausses !)
On obtient alors le théorème dans toute sa splendeur :
Premier théorème d'incomplétude de Gödel : Toute théorie décidablement axiomatisée, cohérente, et contenant l'arithmétique de Peano est incomplète.
En particulier, ce théorème s'applique à ZFC, qui est la théorie usuelle dans laquelle se font les mathématiques !
Je ne suis pas compétent en philosophie et je ne vais pas m'aventurer à explorer les conséquences philosophiques du théorème. Je dois néanmoins avertir qu'il est très facile d'en abuser. Le théorème de Gödel a été utilisé de manière farfelue pour prouver l'existence de Dieu, sa non-existence, l'impossibilité d'une théorie physique qui explique tout l'Univers, et bien d'autres choses. Je vais donc essayer de dissiper quelques malentendus possibles.
Trouvé dans un commentaire ici.
Les axiomes d'une théorie sont parfaitement démontrables dans cette théorie… c'est presque la définition d'un axiome. Si je veux prouver « pour tout n, on a 0 + n = n » dans l'arithmétique de Peano, il me suffit de dire « c'est un axiome, CQFD ». Sans cela, on ne pourrait pas prouver 0 + 4 = 4 !
En construisant la théorie, on ne donne pas de démonstration des axiomes en dehors de la théorie, mais une fois la théorie construite, ils sont parfaitement démontrables à l'intérieur de cette théorie — dire « c'est un axiome » compte comme une démonstration, c'est même la forme la plus simple de démonstration, c'est comme cela que l'on utilise les axiomes pour prouver d'autres propositions.
Le théorème donne des propositions ni prouvables, ni réfutables, ce qui est très différent. Il ne faut pas confondre « vrai » et « prouvable » — le théorème nous apprend justement que ce sont des notions distinctes.
D'abord, il faut souligner que cela n'a pas de sens en général d'affirmer qu'une proposition est « vraie » ou « fausse » dans une logique. Par exemple, imaginons que nous observions des martiens en train de faire des mathématiques et qu'ils écrivent la proposition ঐ + ঐ = ঠ. Il est possible que dans leur langue, la lettre ঐ soit le symbole pour le nombre 2 et la lettre ঠ le symbole du nombre 4, auquel cas ils considéreront que cette proposition est vraie. Mais si pour eux ঐ représente le nombre 2 et ঠ le nombre 5, alors ils considéreront qu'elle est fausse. Cette métaphore explique que la vérité ne fait pas partie du système logique lui-même, elle dépend de l'interprétation de chaque symbole, appelée en termes techniques un « modèle ». Dans un modèle donné, une proposition est soit vraie, soit fausse. En revanche, une proposition peut être vraie dans un modèle et fausse dans un autre.
S'agissant de l'arithmétique1, l'interprétation qu'on « veut » donner aux symboles est clairement définie : 0 est le nombre zéro, + est l'addition, etc. L'arithmétique est construite exprès pour parler des nombres entiers. Donc, pour une proposition de l'arithmétique, on peut dire qu'elle est vraie ou fausse, et on veut dire implicitement qu'elle est vraie ou fausse dans le modèle des nombres entiers. (Il se trouve qu'il existe d'autres modèles, par le théorème de complétude de Gödel, mais il ne sont pas si intéressants.)
Remarque : Il n'est pas interdit de défendre que tout énoncé même arithmétique n'est pas forcément vrai ou faux. Plus subtilement, on peut aussi défendre que certes, tout énoncé est vrai ou faux, mais le but de la logique est aussi de faire d'autres nuances plus fines à l'intérieur du vrai. C'est l'essence de certaines positions sur la logique intuitionniste, qui rejettent le réalisme consistant à croire que les propositions logiques sont vraies ou fausse dans une réalité indépendante de la conscience humaine (et pour lesquelles que les modèles existent formellement mais pas « réellement »). Simplement, il ne faut pas invoquer le théorème de Gödel comme argument. Le théorème de Gödel est parfaitement compatible avec la vision réaliste.
Même si on découvrait un moyen physique de résoudre des problèmes impossibles à résoudre par les machines de Turing ou les autres modèles de calcul équivalents, le théorème de Gödel resterait parfaitement vrai. La validité d'un théorème mathématique ne peut pas être remise en cause par des découvertes physiques.
En revanche, le théorème de Gödel pourrait devenir moins intéressant. Rappelons qu'il porte sur des théories calculablement axiomatisées, c'est-à-dire qu'il doit exister un algorithme — disons une machine de Turing — qui vérifie les démonstrations. Si la thèse de Church-Turing était prise en défaut par je ne sais quel effet de physique quantique ou dans les trous noirs, on peut imaginer que nous aurions accès à un type d'algorithmes plus puissant que les machines de Turing, et nous pourrions construire des preuves invérifiables par un algorithme normal, mais vérifiables par ces algorithmes augmentés, et le théorème ne s'appliquerait pas à ces preuves-là.
Toutefois, il se trouve qu'on peut prouver le théorème sous des hypothèses très faibles (les conditions de prouvabilité de Hilbert-Bernays), qui supposent essentiellement que la logique est capable de raisonner sur elle-même. Même dans un monde de science-fiction complètement improbable où il existe des algorithmes surpuissants, il semble difficile d'imaginer une logique sur laquelle on ne pourrait pas raisonner logiquement (on peut douter que ce soit vraiment une « logique »). Donc, le théorème de Gödel résiste très bien à la science fiction.
Affirmation hautement contestable trouvée dans le texte L'anti-réductionnisme sur le blog d'un chercheur en mathématiques et philosophe, titulaire d'un prix de l'Académie des sciences…
Il est faux de penser que plus les nombres sont grands, moins on les « comprend » et plus on se « rapproche » de l'incomplétude. J'ai déjà souligné que la calculabilité ne se préoccupe pas d'efficacité, de temps de calcul. Si on prend une propriété que l'on sait tester algorithmiquement, rien n'empêche en théorie de la tester sur des nombres très grands. En pratique, cela peut devenir ingérable, mais la plupart du temps, ce n'est pas le vrai problème.
Prenons un exemple précis. La célèbre conjecture de Goldbach affirme que tout nombre pair à partir de 4 peut être écrit comme une somme de deux nombres premiers. Cette conjecture a été vérifiée jusqu'à des nombres de l'ordre du milliard de milliards, et il existe des arguments heuristiques en sa faveur, mais on ne sait pas la démontrer. On ne peut pas exclure qu'un contre-exemple soit découvert un jour, mais la plupart des mathématiciens pensent qu'elle est vraie et que le défi est simplement de le prouver. Pour cela, l'obstacle n'est pas de faire des calculs sur des nombres très grands. La difficulté est plutôt de trouver un argument qui marche pour tous les nombres, sachant qu'il y en a une infinité. Si la conjecture est vraie, alors pour tout n pair à partir de 4, on peut facilement démontrer que n s'écrit comme somme de deux nombres premiers. Il suffit de chercher les deux nombres premiers en question, en testant toutes les possibilités, ce qui donne les preuves « 2 + 2 = 4 donc 4 s'écrit comme somme de deux nombres premiers », « 3 + 3 = 6 donc 6 s'écrit comme somme de deux nombres premiers », « 3 + 5 = 8 donc 8 s'écrit comme somme de deux nombres premiers », « 3 + 7 = 10 donc 10 s'écrit comme somme de deux nombres premiers », etc. Mais cela donne une preuve différente pour chaque n. On ne sait pas trouver une seule preuve qui fonctionne pour toutes les valeurs de n (et on ne peut pas exclure qu'il n'en existe pas, même si cela semble improbable).
En résumé, les grands nombres ne sont pas spécialement plus « compliqués » que les petits nombres. Ce qui crée l'incomplétude est surtout le fait qu'il y a une infinité de nombres.
Le théorème s'applique à une théorie décidablement axiomatisée, cohérente et contenant l'arithmétique. Il est vrai que les théories incohérentes ne sont pas très intéressantes, car elles prouvent absolument tout (et son contraire), mais les autres hypothèses sont aussi importantes.
Par exemple, on peut imaginer la théorie dont les axiomes sont tous les énoncés vrais de l'arithmétique. Cette théorie, appelée « arithmétique vraie », est complète : soit un énoncé est vrai et elle le prouve (parce qu'elle le contient comme axiome), soit un énoncé est faux et elle prouve son contraire (à nouveau parce qu'elle le contient comme axiome). Les preuves dans cette théorie ressemblent à « La conjecture de Goldbach est vraie parce que c'est un axiome »… ce qui ne nous avance pas à grand-chose ! La raison profonde pour laquelle cette théorie ne peut pas servir comme fondement des mathématiques est qu'elle n'est pas calculablement axiomatisée, ses démonstrations sont invérifiables : « La conjecture de Goldbach est fausse parce que c'est un axiome » a tout aussi bien l'apparence d'une démonstration valable, et on ne peut pas algorithmiquement savoir s'il faut l'accepter.
Il y a aussi des quantités de théories intéressantes qui ne contiennent pas l'arithmétique, et qui sont complètes. L'une d'elles est la « théorie des corps réels clos » (c'est le théorème de Tarski-Seidenberg). Intuitivement, alors que l'arithmétique parle des nombres entiers, la théorie des corps réels clos parle des nombres réels (c'est-à-dire tous les nombres possibles, comme 1, -4, 2/3, √2, π, etc., sauf les nombres complexes pour ceux qui les connaissent). Il peut sembler surprenant que cette théorie soit complète, car intuitivement, les nombres réels comme π semblent plus « compliqués » que les nombres entiers. Pourtant, considérons par exemple la proposition « il existe x tel que 7×x = y ». Dans la théorie des corps réels clos, elle est vraie quel que soit y (la solution étant x = y/7). Dans l'arithmétique, elle n'est vraie que pour y multiple de 7. On comprend sur cet exemple que le fait de se restreindre aux nombres entiers peut rendre la théorie plus riche.
Cependant, l'arithmétique fait partie des mathématiques de base, et on souhaite que les preuves mathématiques soient vérifiables, donc le théorème de Gödel s'applique bien à toute théorie qu'on pourrait vouloir prendre comme fondement des mathématiques.
Il faudra m'expliquer en quoi la Bible est une théorie logique qui contient l'arithmétique. Il ne faut pas appliquer le théorème à tort et à travers dans un contexte où il ne s'applique pas.
Pour la théorie des ensembles, la situation est nettement plus délicate, parce que contrairement aux entiers naturels, il n'y a pas un consensus universel sur la notion d'ensemble, même s'il y a une théorie à peu près consensuelle, ZFC. Pour donner un exemple précis, il existe des variantes de la théorie des ensembles où on peut avoir un ensemble qui contient un autre ensemble, qui lui-même contient un autre ensemble, qui à son tour contient un autre ensemble, etc., à l'infini. Dans ZFC, ce n'est pas possible, le processus s'arrête forcément à un moment donné (on tombe sur l'ensemble vide, qui ne contient rien), mais la preuve est décevante : c'est simplement un axiome de ZFC. On peut penser que ces théories des ensembles alternatives ne parlent pas des « mêmes » ensembles, que si elles prouvent des choses différentes, c'est qu'elles n'ont pas la même définition d'un ensemble. Mais alors, que dire d'énoncés ni prouvables ni réfutables dans ZFC comme l'hypothèse du continu, qui affirme qu'il existe un infini de taille strictement comprise entre l'infini des nombres entiers et l'infini des nombres réels ? Toutes sortes de positions existent. On peut penser que l'hypothèse du continu est vraie ; ou bien qu'elle est fausse ; ou bien qu'elle est soit vraie soit fausse mais on ne peut pas le savoir ; ou bien qu'elle n'est ni vraie ni fausse parce qu'il n'y a pas de raison qu'elle soit l'un ou l'autre ; ou bien que la réponse dépend de la définition d'un ensemble, et que ZFC ne définit pas les ensembles de manière suffisamment précise pour trancher.