Chapitre 4. Les limites du raisonnement formel
p. 99-115
Texte intégral
AU COMMENCEMENT ÉTAIENT LES AXIOMES
1Comme nous l’avons vu dans le chapitre précédent, le problème de savoir si l’exécution d’un programme arbitraire d’ordinateur finira par se terminer ne peut se résoudre sur aucune machine de Turing. Bien que, à première vue, ce résultat semble ne concerner que la théorie du calcul, il a des répercussions inattendues sur la nature profonde des mathématiques. Des questions aussi fondamentales que : « les problèmes mathématiques sont-ils tous résolubles ? » et : « y a-t-il un test “mécanique” pour la vérité mathématique ? » sont étroitement liées au problème de l’arrêt.
2La recherche de la sagesse mathématique commence par certaines présuppositions, ou axiomes, dont la vérité est tenue pour acquise. Armés seulement de la pure logique et guidés par leur intuition, les mathématiciens procèdent alors à la dérivation d’autres vérités—les théorèmes. Le grand édifice des mathématiques est ainsi construit, théorème par théorème. La solidité de toute la construction, en supposant une logique sans faille, est alors une conséquence nécessaire de la solidité de ses fondations : si les axiomes sont vrais, les théorèmes le sont tout autant. Le mathématicien grec Euclide fut le premier à utiliser cette approche axiomatique, il y a quelque 2300 ans, pour bâtir la géométrie d’une façon systématique. Jusqu’à tout récemment, les élèves de niveau secondaire pouvaient avoir un aperçu de cette puissante méthode, très révélatrice de la nature déductive des mathématiques, grâce à l’étude de la géométrie dans des manuels basés sur le chef-d’œuvre d’Euclide, Les Éléments. Mais la géométrie selon Euclide (et presque toute la géométrie elle-même) n’a pas survécu aux changements radicaux dans l’enseignement des mathématiques des années 1970. Situation ironique, ceux qui ont conçu les nouveaux programmes avaient eux-mêmes appris les mathématiques selon la manière traditionnelle, sans doute avec succès.
3L’étude des nombres naturels, ou arithmétique, est peut-être la théorie mathématique par excellence. Plusieurs systèmes d’axiomes applicables à l’arithmétique ont circulé au début du XXe siècle, lorsque les questions concernant les fondements des mathématiques étaient très à la mode parmi les mathématiciens et les logiciens. La caractéristique principale de ces axiomes est d’énoncer certaines vérités évidentes à propos des nombres naturels, par exemple : chaque n a un successeur (n+1), ou bien : différents nombres ont des successeurs différents, etc. D’autres systèmes peuvent avoir comme axiomes les lois fondamentales qui régissent les opérations habituelles telles que l’addition et la multiplication. Parmi ces lois, nous trouvons les propriétés de commutativité (n + m = m + n et nm = mn, pour tous les nombres naturels n, m), de distributivité de la multiplication par rapport à l’addition (n(m+k) = nm+nk), etc.
4Chaque propriété des nombres naturels qui peut être inférée logiquement des axiomes est un théorème, et la totalité de tous les théorèmes (démontrés) constitue le réservoir de notre connaissance arithmétique actuelle.
SONDER LES FONDEMENTS
L’instrument qui amène le réglage des différences entre la théorie et la pratique, entre la pensée et l’expérience, sont les mathématiques. Elles établissent le pont et le renforcent continuellement. Ainsi, toute notre culture actuelle, dans la mesure où elle est concernée par la compréhension intellectuelle et par la conquête de la nature, repose sur les mathématiques !
(David Hilbert)1.
5Quels que soient les énoncés que nous choisissions comme axiomes, deux questions s’imposent d’elles-mêmes naturellement (au logicien) : une question portant sur la cohérence, formulée comme suit : « Peut-on jamais déduire une contradiction à partir des axiomes ? », et une question portant sur la complétude énoncée de la façon suivante : « Toutes les vérités (arithmétiques) sont-elles démontrables à partir des axiomes ? » Un système d’axiomes particulier (pour l’arithmétique ou pour une autre branche des mathématiques) est dit cohérent et complet si les réponses aux questions ci-dessus sont respectivement non et oui. Pour paraphraser la formule des tribunaux, les axiomes sont cohérents et complets si on peut logiquement en déduire toute la vérité (complétude) et rien que la vérité (cohérence).
6La question de la cohérence a hanté les mathématiciens et les philosophes depuis longtemps, et, jusqu’à ce jour, n’a reçu aucune réponse concluante2. Bien sûr, les mathématiciens sentent au fond d’eux-mêmes que l’arithmétique est cohérente. En 1924, le distingué géomètre allemand Félix Klein présenta le plaidoyer suivant en faveur de la cohérence : « L’intuition nous montre, écrivait-il, l’existence de nombres pour lesquels ces lois sont valables [la commutativité, la distributivité, etc.] ; par conséquent, il est impossible que des contradictions se cachent dans ces lois »3.
7Mais l’argument de Klein ne persuada pas les soi-disant formalistes, lesquels se méfient de l’intuition et ne croient pas à l’existence des nombres naturels ni d’ailleurs aux autres entités mathématiques. Dans l’univers des formalistes, la seule réalité est celle des marques sur le papier—des expressions dans un langage formel—qu’on peut manipuler selon des règles précises. Puisque ces expressions formelles sont censées n’avoir aucune signification, elles ne sont ni vraies ni fausses. Sur l’autel du pur formalisme, ce n’est pas seulement le sens mais aussi la notion de vérité qui est sacrifiée.
8Le formalisme est généralement associé au nom de David Hilbert, qui a apporté une contribution capitale aux mathématiques et à ses fondements. En fait, le fameux mathématicien allemand était un fervent adepte des mathématiques classiques. L’approche formelle ne constituait pour lui qu’un moyen stratégique en vue d’établir la solidité des méthodes traditionnelles de démonstration—surtout celles qui mettent en jeu le concept d’infini—méthodes qui furent attaquées par un groupe de dissidents qu’on a appelés les intuitionnistes. En 1928, Hilbert s’adressa au Congrès international des mathématiciens de Bologne. Il mit de l’avant comme étant des problèmes majeurs et ouverts les questions de la cohérence et de la complétude de l’arithmétique, ainsi que celle des systèmes plus larges tels que l’analyse mathématique classique. Il ne fait pas de doute que Hilbert tenait ces systèmes formels pour cohérents et complets.
9Une preuve de la cohérence aurait persuadé les sceptiques que la théorie des nombres et l’analyse, ces piliers du temple des mathématiques, étaient exemptes de contradictions internes, garantissant ainsi qu’aucune proposition incongrue telle que 2+2 = 5 ne puisse jamais être déduite. Par ailleurs, une démonstration de la complétude aurait confirmé, selon les mots de Hilbert, « la conviction partagée par tout mathématicien que, bien qu’aucune preuve ne l’ait encore étayée », tout problème mathématique peut être résolu4. Hilbert était aussi convaincu que notre compréhension de la nature et sa conquête éventuelle reposaient sur les mathématiques ; d’où l’importance qu’il attachait à la validation de ses fondements. Au sommet de sa gloire, tout près de la retraite, comment aurait-il pu soupçonner que son programme optimiste allait être, peu de temps après, amèrement contrarié ?
LES LANGAGES FORMELS
10Pour mieux comprendre ce qui est en jeu ici, retournons à Euclide et à sa méthode axiomatique. Quand le célèbre mathématicien écrivit ses fameux Éléments vers 300 av. J.-C., il utilisa un langage naturel—le grec—pour décrire les relations entre les objets géométriques (points, lignes, etc.). Cependant, aujourd’hui, si nous espérons répondre à des questions sur les mathématiques telles que : « l’énoncé S est-il un théorème ? », il nous faut préciser exactement ce qui constitue un énoncé mathématique. Un des moyens à prendre pour ce faire est de recourir à un langage formel. Les langages de programmation utilisés pour écrire les instructions d’un ordinateur sont des exemples de tels langages. Une des différences majeures entre les langages naturels et les langages formels est que ces derniers ont des règles grammaticales très précises, grâce auxquelles il est possible (à nous ou à une machine) de déterminer sans équivoque quelles expressions dans le langage sont des énoncés significatifs.
11Un langage formel approprié à l’écriture d’énoncés concernant les nombres naturels est le langage de l'arithmétique. Son alphabet comprend plusieurs types de symboles : les nombres 0 et 1 ; les lettres a, b,..., x, y, z—qui représentent des nombres naturels arbitraires ; les symboles d’opérations + (pour l’addition) et • (pour la multiplication) ; le symbole d’égalité (-) et les symboles logiques ¬ (non), v (ou), & (et), =>((si... alors), ∃ (pour quelque) et ∀ (pour tout). Les expressions significatives du langage sont des chaînes de symboles tirés de cet alphabet et formées d’après certaines règles précises de syntaxe—qu’il serait trop fastidieux de préciser ici. Chaque expression (significative) dit « quelque chose » au sujet des nombres naturels. Par exemple,
12∀ x (x+x =x • x => (x =oνx =1+1)) (1)
13se lit, lorsque traduit en français : « Si un nombre ajouté à lui-même égale son carré, alors le nombre est soit 0 soit 2 », tandis que
14∀ x ((¬∃z (¬(z = 1) & ¬ (z = x) & ∃ y (y • z = x)) & ¬ (x =1))
15=>∃ w(w+1+1+1 =x)) (2)
16signifie : « Chaque nombre premier est supérieur ou égal à 3 ».
17La parfaite connaissance des règles syntaxiques du langage formel est, bien entendu, nécessaire pour effectuer la traduction. Une traduction littérale de (2) serait : « Pour tout (nombre naturel) x, s’il n’existe pas de z tel que z n’égale pas 1 et que z n’est pas égal à x et, pour quelque y, y • z =x et x≠1[en d’autres mots, si nul nombre autre que 1 et x lui-même divise x et x n’est pas égal à 1—ce qui équivaut à “si x est premier”], alors il existe w tel que w+3 = x [autre moyen de dire “alors x est supérieur ou égal à 3”] ». Cet exemple illustre un des inconvénients des langages formels comme moyen de communication : les phrases deviennent vite trop longues et difficilement compréhensibles.
18Une grande partie de la théorie des nombres peut être formulée dans ce langage formel. Des énoncés, tels que (1) ci-dessus, sont vrais (comme on peut facilement le vérifier en résolvant l’équation 2x =x2), alors que d’autres sont faux. L’énoncé (2) est évidemment faux, car 2 est un nombre premier plus petit que 3. Pour déclarer que ces deux énoncés sont respectivement vrai et faux, nous avons fait appel à notre connaissance des nombres naturels et de leurs opérations. Cependant, pour la plupart des énoncés formels, une décision concernant leur vérité ou leur fausseté est beaucoup plus difficile à obtenir. Le jury est encore occupé à délibérer sur des propositions aussi innocentes en apparence que « chaque nombre pair supérieur à 2 est la somme de deux nombres premiers » (la fameuse conjecture de Goldbach). L’assertion est vraie, par exemple, des nombres 4 (= 2+2), 20 (= 17+3), 66 (= 59+7), et de beaucoup d’autres. À vrai dire, personne n’a encore trouvé un nombre pair qui ne soit pas la somme de deux nombres premiers ; mais personne non plus n’a démontré qu’un tel nombre ne peut exister ; donc la question n’est toujours pas résolue. Si nous échouons dans nos tentatives pour découvrir si un énoncé donné est vrai ou faux, quelqu’un qui s’y connaît davantage ou qui est plus ingénieux pourra éventuellement réussir. Ce « quelqu’un » pourrait-il être une machine ?
LES MATHÉMATIQUES MÉCANIQUES
19Dans son discours de 1928 à la communauté mathématique, David Hilbert s’était également demandé si les mathématiques sont décidables. Par ceci, il voulait dire : existe-t-il une méthode précise, semblable à un procédé « mécanique », qui pourrait, une fois appliquée à un énoncé mathématique arbitraire, dire si celui-ci est vrai ou faux ? Quelques années plus tard, Alan Turing précisa la notion de « procédé mécanique » avec la définition de sa machine, de sorte que la question peut maintenant se poser ainsi : y a-t-il une machine de Turing qui, après avoir lu un énoncé mathématique qu’on lui aurait soumis, finirait par nous dire si cet énoncé est vrai ou faux ?
20Si une telle machine existait (nous l’appellerons MD, ou machine de Turing à décision), nous pourrions l’utiliser pour résoudre le problème de l’arrêt. Voici comment. Supposons que nous désirions savoir si la machine de Turing T va finalement s’arrêter, après été mise en marche avec un ruban d’entrée ne contenant que des zéros. On peut démontrer—mais les détails techniques sont longs et fastidieux—qu’il existe un énoncé H dans le langage formel de l’arithmétique, lequel, traduit en français, dit : « La machine de Turing T va finalement s’arrêter après avoir été mise en marche avec un ruban d’entrée ne contenant que des zéros ». Or on peut démontrer—mais les détails techniques sont longs et fastidieux—qu’il existe un énoncé H dans le langage formel de l’arithmétique, lequel, traduit en français, dit : « La machine de Turing va finalement s’arrêter après avoir été démarrée avec un ruban d’entrée ne contenant que des zéros. » Nous pourrions alors poser la question « Est-ce que H est vrai ? » à la MD, qui, tôt ou tard, serait tenue de répondre. À ce moment-là, nous saurions que T s’arrêtera en fin de compte (si la réponse de la MD est oui) ou qu'elle poursuivra sa marche pour toujours (si elle est non).
21Comme le problème de l’arrêt ne peut être résolu, la MD ne peut pas davantage exister. Bref, il n’y a pas de test mécanique pour les vérités concernant les nombres naturels—encore moins pour les vérités mathématiques en général. Si les mathématiciens veulent découvrir la vérité, ils doivent emprunter un chemin plus difficile : la démonstration de théorèmes—ils ne peuvent s’attendre à ce que la machine fasse le travail à leur place.
LA LOGIQUE MÉCANIQUE
22Une des choses qu’une machine de Turing peut faire est de vérifier la validité de certaines preuves mathématiques. Pour la vérification par la machine, une preuve présumée, disons de S, doit être écrite comme une suite E1, E2,E3,..., S d’expressions formelles—la dernière étant S—de sorte que chaque expression dans la séquence ou bien est un axiome ou bien peut être logiquement déduite des expressions qui la précèdent. Il faut faire remarquer qu’il s’agit ici d’une version condensée et formelle de notre idée intuitive de preuve, à savoir une chaîne de faits qui sont ou bien incontestablement vrais (les axiomes) ou bien sont les conséquences logiques de faits établis auparavant.
23La machine de Turing vérificatrice (appelons-la MV) prend comme entrée une suite E1, E2, E3,..., S et donne comme sortie oui, si la séquence est une preuve (de S) et non si elle ne l’est pas. Écrire un programme pour MV est plutôt simple à l’exception d’un détail : il faut pouvoir dire à la machine, en un nombre fini d’instructions, comment reconnaître un axiome quand elle en voit un. Ceci peut se faire facilement s’il n’y a qu’un nombre fini d’axiomes—par exemple, en donnant à la machine, convenablement encodée, la liste complète de ceux-ci. Mais si les axiomes sont en nombre infini, l’existence de MV dépendra de notre aptitude à condenser l’information nécessaire pour détecter un axiome en un ensemble fini d’instructions.
24Il nous faut aussi enseigner à MV comment vérifier si Ei découle logiquement de certaines des expressions E1, E2, E3,..., Ei-1 qui la précèdent. Heureusement, des logiciens ont résolu ce problème pour nous depuis longtemps en réduisant l’inférence logique à l’application de quelques règles formelles très explicites. Ces règles sont tellement « mécaniques » qu’une machine de Turing peut les comprendre. Ainsi, en testant de façon séquentielle E1, E2, E3,..., pour un axiome ou une conséquence logique, MV peut nous dire si oui ou non cette séquence est une preuve.
25Pour résumer, une machine de Turing peut très bien vérifier la logique d’une preuve, mais elle peut avoir du mal à reconnaître les axiomes. Quand les preuves concernent des propositions arithmétiques, cette insuffisance s’avérera un obstacle insurmontable.
LES LIMITES DU RAISONNEMENT FORMEL
26Nous pouvons maintenant répondre à l’une des questions de David Hilbert : l’arithmétique est-elle complète ? Ou, plus explicitement : y a-t-il un ensemble d’axiomes desquels peuvent être logiquement déduites toutes les vérités concernant les nombres naturels ? La réponse brève est non. C’est un jeune logicien autrichien qui révéla la mauvaise nouvelle en 1930, à peine trois ans après que Hilbert eut soulevé la question avec beaucoup d’espoir à Bologne. Dans un article qu’il présenta à l’Académie des sciences de Vienne, Kurt Gödel rendait publics ses résultats, maintenant connus sous le nom de premier théorème d’incomplétude de Gödel : aucun système formel d’axiomes n’est assez puissant pour prouver tous les énoncés arithmétiques vrais, si nous exigeons que la notion de preuve soit elle-même formelle, c’est-à-dire vérifiable par quelque « test mécanique »—un programme informatique, par exemple. (Il y a un deuxième théorème d’incomplétude, concernant la question de la cohérence.)
27Dès sa publication en 1931, la découverte de Gödel suscita d’innombrables comptes rendus tant techniques que de vulgarisation : articles, essais et livres de mathématiciens et de philosophes parmi les plus compétents. Pourquoi encore essayer ? Parce que, comme l’écrivit Ivar Ekeland dans l’introduction à son excellent ouvrage Mathematics and the Unexpected : « [...] il y a encore quelque chose à dire, et que la même vieille histoire peut être racontée d’une autre façon »5.
28Laissons le jeune Gödel lui-même (il n’avait alors que 25 ans) nous présenter sa découverte :
Le développement des mathématiques vers une plus grande précision a conduit, comme tout le monde le sait, à la formalisation de certaines de leurs grandes zones, de sorte qu’un très petit nombre de règles mécaniques peuvent servir à la démonstration de n’importe quel théorème. Les systèmes formels les plus englobants qui aient été établis jusqu’ici sont celui des Principia Mathematica, d’Alfred Whitehead et Bertrand Russell, en 1925, d’une part, et le système axiomatique de la théorie des ensembles de Zermelo-Fraenkel (que J. von Neumann a développé davantage), d’autre part. La généralité de ces deux systèmes est telle qu’ils contiennent, déjà formalisées, toutes les méthodes de preuve utilisées aujourd’hui en mathématiques, c’est-à-dire quelles se ramènent à quelques axiomes et règles d’inférence. On pourrait alors présumer que ces axiomes et règles d’inférence suffisent à trancher toute question mathématique formellement exprimable dans ces systèmes. Nous verrons plus bas que tel n’est pas le cas, et qu’au contraire il y a dans les deux systèmes mentionnés des problèmes relativement simples dans la théorie des nombres entiers qui ne peuvent être tranchés sur la base des axiomes6.
29La dernière phrase signifie qu’il y a des propositions S indécidables qu’on ne peut ni prouver ni réfuter, autrement dit ni S ni sa négation ne peuvent se déduire des axiomes—quoique l’un de ces deux énoncés soit nécessairement vrai. C’est en ce sens que les systèmes d’axiomes mentionnés par Gödel sont « incomplets » : parce que toutes les vérités arithmétiques ne peuvent pas en être logiquement dérivées.
30Voici les grandes lignes de l’argument de Gödel. Grâce à l’utilisation d’une astucieuse méthode d’encodage, qu’on appellera plus tard le numérotage de Gödel, à chaque expression formelle peut être attribué un nombre naturel. Dès lors, des expressions formelles prétendant dire quelque chose au sujet des nombres naturels peuvent être également interprétées comme affirmant quelque chose à propos d’autres expressions formelles. Plus particulièrement, Gödel montre par un argument ingénieux l’existence d’une expression G qui affirme quelque chose à propos d’elle-même, assertion qui équivaut à peu près à ceci : « Je ne suis pas formellement démontrable ». Par conséquent, si G est fausse, alors un énoncé faux—G—peut se déduire des axiomes. Or nous devons évidemment exclure cette possibilité si nous voulons que notre formalisation soit cohérente. Donc, G doit être vraie : vérité arithmétique qui ne peut être logiquement déduite des axiomes.
31Ainsi donc, contrairement à la croyance largement répandue, vérité et déductibilité sont deux choses différentes—conclusion riche de conséquences pour ceux qui s’intéressent à la philosophie des mathématiques. Toutefois, selon l’optique des formalistes, les énoncés mathématiques sont purement et simplement des chaînes de symboles sans interprétations, et de ce fait ne sont ni vrais ni faux. L’affirmation que la vérité n’est pas la même chose que la déductibilité est alors dénuée de sens ; car il n’y a pas vérité mais seulement déductibilité.
D’UN PROBLÈME INSOLUBLE À UN AUTRE
32En un certain sens, si l’arithmétique n’est pas complète, c’est à cause de l’insolubilité du problème de l’arrêt. Mais nous pourrions présenter les choses autrement et dire que c’est l’incomplétude de l’arithmétique qui explique que le problème de l’arrêt n’a pas de solution. En fait, l’incomplétude et la question de l’arrêt constituent des problèmes équivalents. Par là, nous voulons dire qu’une solution de l’un peut servir à trouver la solution de l’autre, de telle sorte que l’un et l’autre soient résolubles ou aucun des deux ne le soit (ou ils coulent ensemble ou ils nagent ensemble).
33En mettant en évidence cette interdépendance, nous allons exposer les grandes lignes d’une autre preuve du théorème de Gödel. Notre argument peut se résumer comme suit : la complétude de l’arithmétique entraînerait l’existence d’une MD (la machine de Turing à décision) ; or, comme nous l’avons déjà montré, il serait alors possible, grâce à une MD, de construire une (autre) machine de Turing qui, elle, pourrait résoudre le problème de l’arrêt—une machine qui ne peut exister. En une seule phrase : si l’arithmétique était complète, le problème de l’arrêt pourrait être résolu ; mais comme celui-ci ne le peut pas, nous devons conclure que celle-là non plus ne peut l’être.
34Supposons que A soit un ensemble d’axiomes duquel toutes les vérités arithmétiques peuvent être dérivées par l’utilisation (formelle) des règles d’inférence. Voici une recette pour construire une MD. Pour décider si l’énoncé S dans le langage de l’arithmétique est vrai ou faux, nous alimentons MV (la machine de Turing vérificatrice) avec toutes les suites finies possibles E1, E2, E3,..., En, l’une après l’autre, d’expressions significatives. (Il existe certainement un nombre infini de telles suites, mais un argument standard montre qu’elles peuvent être systématiquement engendrées par une machine de Turing.) Rappelons-nous qu’une MV répondra « oui » si la suite d’entrée est une preuve (de la dernière expression En dans la suite), et « non » si elle ne l’est pas. Maintenant, ou S est vrai ou sa négation, nonS, l’est—ce que nous savions déjà, bien entendu. Étant donné que toutes les vérités peuvent être dérivées de A, il y a ou bien une preuve formelle de S ou une preuve formelle de non-S. Quel que soit le cas, cette preuve entrera tôt ou tard dans MV et suscitera une réponse affirmative. À ce moment-là nous saurons que S est vrai—si MV a trouvé une preuve de S—ou que S et faux—si MV a découvert une preuve de non-S.
LA MACHINE MIRACULEUSE N’EXISTE PAS
Seul un profane inculte peut s’imaginer que les mathématiciens font des découvertes en faisant tourner la manivelle d’une machine miraculeuse.
(Godfrey H. Hardy.)
35Il existe certainement des ensembles d’axiomes à partir desquels peuvent être dérivées toutes les vérités arithmétiques. Par exemple, nous pouvons prendre comme axiomes l’ensemble de tous les énoncés vrais. Alors, toutes les vérités arithmétiques seraient (banalement) démontrables : une preuve de la vérité de S serait simplement S elle-même. Mais de tels ensembles complets ne sont pas reconnus par les machines de Turing ; par conséquent, les preuves qui s’appuient sur eux ne peuvent être formalisées. Bref, aucun système axiomatique pour l’arithmétique ne peut être à la fois formel et complet. Pour Aubert Daigneault, mathématicien à l’Université de Montréal, Gödel a prouvé que, lorsque nous parlons de « nombres naturels », nous ne pouvons pas dire précisément ce dont nous parlons—ce qui signifie que nous ne pouvons pas décrire les nombres naturels par un ensemble d’axiomes explicites, « mécaniquement » vérifiables.
36Pour vraiment mesurer le caractère définitif du coup de grâce que Gödel a porté au rêve épistémologique de Hilbert (celui de prouver toutes les vérités mathématiques à partir d’un simple ensemble d’axiomes), il faut comprendre toute l’importance de son théorème d’incomplétude. Car le jeune mathématicien autrichien a non seulement montré que certains systèmes particuliers sont incomplets, mais aussi que chaque système formel pour l’arithmétique s’avérera incomplet : il y aura toujours des vérités arithmétiques, exprimables dans le langage formel, qui ne sauront être prouvées formellement. Il est donc impossible de confiner la théorie des nombres— encore moins toutes les mathématiques—dans le cadre d’un système formel. Les mathématiciens devraient se sentir soulagés par la nouvelle que leur science ne peut pas se réduire, même en principe, à un jeu formel auquel les machines peuvent jouer.
UN PROBLÈME DE COLORATION
37Malgré sa profondeur et son caractère définitif, le théorème d’incomplétude de Gödel reste un résultat théorique à propos des limites d’une entreprise particulière : la formalisation des preuves mathématiques. Résultat, après tout, dont les conséquences sont plus philosophiques que pratiques. Ce fut, pour certains, la fin d’un rêve qui leur rappelait étonnamment un autre rêve brisé, celui, entretenu par les scientifiques du XVIIIe siècle, de la croyance en un univers prévisible réglé comme une horloge selon les lois de Newton.
38Mais la fin d’un rêve marque souvent le début d’une meilleure appréciation de la réalité. Tous les problèmes mathématiques n’ont peut-être pas de solution, mais la grande majorité d’entre eux en ont7, et la vérité peut encore être découverte en dehors de la rigidité d’un système formel. Les mathématiques peuvent très bien être exemptes de contradictions, malgré l’absence d’une preuve de leur cohérence. Et même si une contradiction apparaissait, les ponts d’acier et de ciment dont la construction a utilisé des principes mathématiques ne s’effondreraient pas pour autant, comme Stanislaw Ulam l’a déjà noté (Ulam était un mathématicien polonais qui a travaillé avec les meilleurs scientifiques de son époque à Los Alamos, pendant la Seconde Guerre mondiale).
39Nous avons déjà vu les faiblesses des ordinateurs numériques (même idéaux) dans la découverte de la vérité mathématique. Les ordinateurs ne peuvent être programmés pour prouver tous les théorèmes, mais, comme outils pour aider les mathématiciens dans certaines preuves, ils sont non seulement précieux mais parfois même pourraient être essentiels.
40Le casse-tête mathématique connu comme le problème des quatre couleurs a eu une histoire longue et colorée8. Les écoliers depuis des siècles colorient des cartes dessinées sur des feuilles de papier en utilisant différentes couleurs pour peindre les pays limitrophes, et probablement sans jamais se soucier du nombre de couleurs dont ils ont vraiment besoin. Un coup d’œil sur la carte de l’Amérique du Sud révélerait que le Paraguay, la Bolivie, le Brésil et l’Argentine sont peints en couleurs différentes—comme il se doit, puisque chaque pays partage une frontière avec les trois autres. De sorte qu’il nous faut au moins quatre couleurs. En 1852, Francis Guthrie, étudiant au London University College, constata qu’une palette de quatre couleurs semblait suffisante pour colorier n’importe quelle carte ; il se demanda ensuite si sa thèse pouvait être démontrée mathématiquement (ça prend un étudiant pour demander une chose pareille !). La question avait paru réglée en 1879 lorsqu’Alfred Kempe, un avocat, proposa justement une telle preuve mathématique. Mais, onze ans plus tard, des mathématiciens découvrirent une faille dans son argumentation. La question de la conjecture des quatre couleurs était de nouveau posée. Pour résumer, disons simplement que le problème fut finalement résolu en 1976 par Kenneth Appel et Wolfgang Haken9, deux mathématiciens de l’Université de l’Illinois. Mais leur preuve n’était pas une preuve traditionnelle « écrite sur papier » qu’un autre mathématicien aurait pu vérifier. Non seulement des parties de la preuve avaient été réalisées par une machine, mais sa validité elle-même ne pouvait être vérifiée qu’avec l’aide d’un ordinateur.
41La recherche d’une preuve rigoureuse commence par la traduction du problème considéré en un langage mathématique. Premièrement, nous représentons chaque pays par un point ; puis on relie par une ligne chaque paire de points représentant des pays voisins. (Une clarification s’impose ici : les pays voisins doivent partager une frontière qui n’est pas qu’un seul point, sinon il n’y aurait aucune limite au nombre de couleurs nécessaires. Pour vous en rendre compte, pensez à ces pays comme à des pointes de tarte découpées mais n’ayant pas encore été servies. Sans cette convention, deux tranches quelconques seraient voisines [leurs pointes se toucheraient] et donc nous aurions besoin d’autant de couleurs qu’il y a de tranches.) La carte originale est ainsi remplacée par un graphe (figure 2.3) et la coloration des pays par le coloriage des sommets. La condition selon laquelle les pays adjacents ne doivent pas partager la même couleur sera alors remplie si les sommets reliés par un côté sont « peints » en des couleurs différentes.
42Nous appellerons pentachromatique un graphe qui ne peut être peint en moins de cinq couleurs. La fameuse hypothèse de Guthrie au sujet de la coloration des cartes peut maintenant être présentée dans les termes abstraits suivants : il n’existe aucun graphe pentachromatique. Or nous ne savons pas si des graphes pentachromatiques existent, mais supposons que ce soit le cas. Alors l’un d’entre eux, appelons-le M, doit avoir le plus petit nombre de sommets—autrement dit, aucun autre graphe pentachromatique n’a moins de sommets que M. Pour résoudre le problème des quatre couleurs, il suffit de prouver que M ne peut exister.
43Dans la première partie de leur preuve, Appel et Haken ont construit une liste de 1834 petits graphes appelés configurations et ont prouvé, dans le sens traditionnel du terme, qu’au moins l’une d’entre elles doit nécessairement faire partie de n’importe quel graphe. Ensuite, leur programme informatique vérifia que chacune de ces configurations « inévitables » possédait une certaine propriété que le graphe pentachromatique minimal M ne pouvait posséder. En combinant l’argument des mathématiciens et les résultats de l’ordinateur, nous obtenons une preuve que la conjecture de Guthrie est fondée : quatre couleurs suffisent.
LA REVANCHE DE L’ORDINATEUR
44La solution de Appel et Haken fut le premier exemple d’une preuve assistée par ordinateur. Elle comportait des résultats obtenus avec l’aide d’un ordinateur qui ne pouvaient pas être « manuellement » vérifiables, comme peuvent l’être les preuves mathématiques traditionnelles. En 1989, Herbert Wilf et Doron Zeilberger, tous deux de l’Université de Pennsylvanie, écrivirent un programme informatique qui démontre certaines identités combinatoires10. Ces identités sont essentiellement des équations qui affirment que deux façons différentes de compter les objets dans un ensemble— l’une compliquée, l’autre simple—sont en fait égales. Mais les preuves de Wilf et Zeilberger ne dépendent pas vraiment de l’ordinateur, parce que les données de sortie de la machine peuvent être converties en une preuve ordinaire. En revanche, une preuve véritablement assistée par ordinateur ne nous laisse aucun autre choix que celui de croire l’ordinateur. Naturellement, une telle dépendance envers les machines pour régler une question purement mathématique—l’hypothèse des quatre couleurs, par exemple—en a troublé quelques-uns. Les mathématiciens n’ont pas l’habitude de se fier à une preuve de seconde main quand il s’agit de démontrer des théorèmes.
45Quelques années plus tard, en 1988, un autre résultat controversé était annoncé. Un superordinateur Cray-1A avait résolu un problème mathématique très ancien, à savoir : existe-t-il un plan projectif d’ordre 10 ? Un plan projectif est fait de « points » et de certains ensembles de points appelés « droites ». Le plan est d’ordre n s’il contient exactement n2+n+1 points et autant de droites, et à condition que les quatre axiomes suivants soient satisfaits : chaque droite est faite de n +1 points ; chaque point se situe sur n + 1 droites ; deux droites quelconques (distinctes) ont exactement un point en commun ; deux points quelconques (distincts) se situent sur exactement une droite.
46Certaines conditions sur n garantissent l’existence d’un plan projectif de cet ordre. Par exemple, si n = pm, pour un nombre premier p et l’exposant m =1, 2, 3,..., il y a toujours un plan projectif d’ordre n. D’autres conditions, si elles ne sont pas remplies par n, impliquent qu’il n’y a pas de plan d’ordre n. On savait depuis longtemps qu’il existe des plans projectifs de chaque ordre n≤9, excepté n =6. Le plus petit ordre n pour lequel l’existence ou la non-existence d’un plan projectif restait un problème ouvert était n =10.
47Ce qui rend l’ordinateur particulièrement adapté à la recherche de plans projectifs, c’est le fait qu’un plan projectif peut être concrètement représenté comme une matrice binaire (cette matrice « d’incidence » a un 1 dans la iième ligne et la jiéme colonne précisément si le jième point se situe sur la iième droite). De cette manière, la recherche d’un plan hypothétique d’ordre 10 devient la chasse à un treillis de 0 et de 1 avec 111 (= 102+10+1) lignes et autant de colonnes, remplissant certaines conditions. Par exemple, chaque ligne doit contenir 11 uns et 100 zéros, pour refléter le fait que chaque droite est constituée de 11 points ; il doit y avoir aussi exactement 11 uns dans n’importe quelle colonne (puisque chaque point doit se situer sur 11 droites).
48Un rapide calcul montre qu’un examen direct par ordinateur, cas par cas, de toutes les matrices binaires 111 par 111 doit être exclu, parce quelles sont beaucoup trop nombreuses. Même sur un superordinateur capable d’effectuer un billion(1012) d’opérations par seconde, le travail prendrait environ 103680 années pour être mené à terme. L’énormité d’un tel nombre est difficile à saisir. Sous forme décimale, 103680 s’écrit 1 suivi de 3680 zéros, alors que l’estimation généreuse de l’âge de l’univers est (selon une théorie cosmologique en vogue) un « petit » 20 milliards (2 x 1010) d’années, ou 2 suivi de 10 zéros. Clement Lam, Larry Thiel et Stanley Swiercz de l’Université Concordia à Montréal en sont arrivés, par des arguments théoriques, à réduire le nombre de matrices à une taille plus raisonnable (mais toujours astronomique). Puis, ils ont écrit une série de programmes pour que l’ordinateur prenne la relève dans cette recherche. Lorsque la machine eut achevé son calcul sans trouver de matrice avec les caractéristiques requises, les trois chercheurs en conclurent qu’aucun plan projectif d’ordre 10 ne pouvait exister. S’il y en avait un, l’ordinateur l’aurait trouvé, est en substance leur argument11. Or une vérification « manuelle » de la recherche infructueuse de l’ordinateur était, évidemment, hors de question. Pas étonnant qu’une telle « preuve » ait laissé beaucoup d’experts sceptiques et le public en général perplexe. Même le New York Times entra dans le débat : « Une preuve mathématique est-elle une preuve si personne ne peut la vérifier ? » titrait un article paru le 20 décembre 1988.
49L’emploi des ordinateurs dans les preuves introduit un élément d’incertitude dont les mathématiciens, contrairement à ceux qui travaillent en sciences expérimentales, n’ont pas l’habitude, et qu’ils seraient réticents à accepter. Dans ce contexte, l’ordinateur est en fait une extension de l’esprit du mathématicien, exactement comme le télescope et le radiotélescope sont des extensions des sens du physicien. Comme le suggèrent les exemples ci-dessus, certaines propositions ne pourraient être prouvées qu’à l’aide de cette extension ; dans de tels cas, la machine devient le partenaire indispensable du mathématicien. Ainsi, malgré leurs limites théoriques, la participation des ordinateurs numériques à la recherche de la vérité mathématique pourrait encore s’avérer incontournable.
Notes de bas de page
1 C. Reid, Hilbert, Berlin-Heidelberg, Springer-Verlag, 1970.
2 E. Nelson, « Taking Formalism Seriously », The Mathematical Intelligencer, 15, no 3 (1993), PP. 8-11.
3 F. Klein, Elementary Mathematics from an Advanced Standpoint, New York, The Macmillan Company, 1932.
4 C. Reid, Hilbert, p. 174.
5 1. Ekeland, Mathematics and the Unexpected, Chicago (IL), University of Chicago Press, 1988.
6 K.Gödel « On formally undecidable propositions of Principia Mathematica and related Systems 1 » (trad. anglaise), dans J. Van Heijenoort (éd.), From Frege to Gödel, a Source Book in Mathematical Logic, 1879-1931. A Collection Of Original Articles, Cambridge (MA), Harvard University Press, 1967. Traduction française de l’ouvrage de Gödel : Le théorème de Gödel (trad. J.-B. Scherrer), Paris, Seuil, 1989.
7 Au sujet de l’existence de problèmes insolubles, on sait depuis l’époque de Gödel qu’il existe des propositions indécidables dans l’arithmétique ordinaire. Cependant, la plupart d’entre elles sont des constructions abstraites, sans aucune signification mathématique. Depuis 1931, les mathématiciens ont cherché un exemple strictement mathématique d’une proposition indécidable, une proposition qui soit mathématiquement simple et intéressante et ne requière pas le codage numérique de notions d’ordre logique. Les premiers exemples de cette sorte n’ont été trouvés qu’en 1977. Le plus frappant parmi ceux-ci était un théorème relativement naturel de combinatoire finie, simple extension du théorème fini de Ramsey (voir J. Paris et L. Harrington, « A Mathematical Incompleteness in Peano Arithmetic », dans J. Barwise (éd.), Handbook of Mathematical Logic, Amsterdam, North-Holland, 1977). Dans un article beaucoup plus récent, on montre que, d’un point de vue topologique, l’ensemble des propositions dont on ne peut prouver la vérité dans un système axiomatique constituent l’immense majorité (C. Calude, H. Juergensen et M. Zimand, « Is Independence an Exception ? », Applied Mathematical Computing, 66 (1994), pp. 63-76).
8 Le reste de cette section et la section suivante s’inspirent de l’article de l’auteur « The Burden of Proof is on the Computer », dans New Scientist, vol 129, no 1757 (1991), pp. 38-40.
9 K. Appel et W. Haken, « Every Planar Map is Four-Colorable », Bulletin of the American Mathematical Society, vol. 82 (1976), pp. 711-712.
10 H. S. Wilf et D. Zeilberger, « Rational Functions Certify Combinatorial Identities », dans Journal of the American Mathematical Society, janvier 1989.
11 C. W. H. Lam, L. Thiel et S. Swiercz, « The Non-Existence of Finite Projective Planes of Order 10 », Canadian Journal of Mathematics, vol xli, no 6 (1989), pp. 1117-1123.x
Le texte seul est utilisable sous licence Licence OpenEdition Books. Les autres éléments (illustrations, fichiers annexes importés) sont « Tous droits réservés », sauf mention contraire.
Guide méthodologique universitaire
Un programme en 12 semaines
Aude Jimenez et Jamal-Eddine Tadlaoui
2011
Éloge du flou
Aux frontières des mathématiques et de l’intelligence artificielle
Arturo Sangalli
2001