Fondements des mathématiques/Des preuves de cohérence

Début de la boite de navigation du chapitre

Ce chapitre expose des preuves de cohérence des principes mathématiques. Il est plus audacieux que les précédents, pour lesquels presque tous les résultats présentés sont connus et prouvés depuis des décennies.

fin de la boite de navigation du chapitre

Comment prouver la fiabilité des principes ?

Les preuves de la vérité et de la fiabilité des principes sont confrontées à un problème de circularité : à partir de quels principes peut-on prouver la fiabilité des principes ? L’examen de ce problème requiert quelques préliminaires.

Qu’est-ce qu’une preuve ?

L’un des principes mathématiques les plus importants est que les vérités doivent être prouvées. Une part importante du travail mathématique consiste précisément à imaginer et à écrire des preuves.

La façon la plus ordinaire de penser à une preuve est de la définir comme une progression par étapes de prémisses vers une conclusion. Si les prémisses sont vraies et si la progression est logique alors la conclusion est prouvée. La logique du premier ordre donne une définition précise et complète de la notion de progression logique et de preuve formelle.

Quand elles sont définies de cette façon, les preuves sont définies avec précision, mais elles sont seulement des moyens pour trouver de nouvelles vérités à partir de vérités déjà connues. Dans une théorie mathématique, tous les théorèmes sont ainsi prouvés à partir des axiomes. Si nous voulons que les théorèmes soient vrais, il nous faut des axiomes vrais. Mais comment savoir que les axiomes sont vrais ?

Comment prouver la vérité des axiomes ?

Leibniz a posé en principe que tout axiome, tout principe, doit être prouvé. Mais il n’a pas dit très précisément comment le faire. À partir de quels principes peut-on prouver la vérité des principes ?

Pour prouver que quelque chose est vrai, il faut avoir une idée de la vérité. La théorie des modèles donne une telle idée et un moyen de prouver qu’un axiome est vrai. Un système d’axiomes est vrai quand il y a un modèle pour lui. Il suffit de trouver un modèle et la vérité de tous les axiomes est automatiquement établie. C’est vrai pour toutes les formules, pas seulement les axiomes. Pour prouver la vérité d’une formule, il faut prouver qu’elle est vraie dans un modèle. Mais habituellement une formule est prouvée à partir d’axiomes et le modèle, s’il existe, est seulement implicite. Cela suffit pour prouver la vérité de cette formule dans le modèle pourvu que l’on sache déjà que les axiomes y sont vrais et que les déductions logiques soient valides.

Cette définition de la vérité par la théorie des modèles laisse cependant des questions sans réponses. Comment prouve-t-on que des axiomes sont vrais dans un modèle ? Un modèle est défini avec des ensembles et des fonctions. Si on veut prouver qu’un modèle existe pour un système d’axiomes, on a besoin d’une théorie des ensembles et des fonctions.

Il semble qu’il y a un cercle vicieux dans cette approche de la vérité mathématique. Pour prouver qu’une théorie est vraie, il faut prouver l’existence d’un modèle. Mais pour cela, on a besoin d’une théorie des ensembles, et plus précisément d’une vraie théorie des ensembles. Mais comment sait-on que cette théorie est vraie ?

Quand on dit qu’une théorie des ensembles est vraie, on veut dire bien sûr qu’elle est cohérente, mais on veut dire plus que cela. Une théorie cohérente n’est pas forcément une théorie des ensembles. La notion première, ou concept fondamental, des théories des ensembles est la relation binaire d’appartenance. Tout être rationnel a une compréhension intuitive de cette notion. Rien qu’avec les ensembles finis on peut lui trouver de nombreuses applications. L’axiome d’extensionalité, selon lequel deux ensembles sont égaux s’ils ont les mêmes éléments, et d’autres loi générales sur les constructions élémentaires des ensembles sont connus de façon intuitive. On peut formuler des théories axiomatiques en accord avec ces connaissances intuitives du concept d’appartenance à un ensemble.

Les connaissances intuitives conduisent parfois à des contradictions, même quand on fait attention à supprimer toute équivoque. Qu’une théorie des ensembles est intuitive ne prouve donc pas qu’elle est vraie. Si en revanche on a prouvé pour une théorie des ensembles qu’elle est cohérente, et si en plus elle est en accord avec nos connaissances intuitives sur les ensembles, alors on peut estimer que cela suffit pour prouver la vérité de cette théorie. On peut alors se reposer sur elle pour prouver l’existence de modèles et donc la vérité d’autres théories. Une théorie des ensembles est une sorte de théorie universelle, au sens où elle permet de raisonner sur toutes les théories.

Mais il y a ici une circularité. Pour prouver qu’une théorie des ensembles est cohérente par la théorie des modèles, il faut prouver l’existence d’un modèle, c’est-à-dire un ensemble, qui est un univers de tous les ensembles de cette théorie. Pour échapper à cette circularité, on pourrait songer à prouver la cohérence de la théorie d’une façon directe, sans passer par la preuve d’existence d’un modèle. Mais on n’y échapperait pas non plus, parce qu’alors il faut raisonner sur toutes les conséquences que l‘on peut déduire logiquement des axiomes et cela revient à définir l’ensemble de toutes ces conséquences et à prouver qu’il ne contient pas de contradiction. Dans ce cas aussi, on a donc besoin d’une théorie des ensembles.

Toute preuve de la fiabilité des principes de preuve a quelque chose de circulaire. Mais ce cercle n’est pas vicieux, ou pas trop, au sens où il ne remet pas en question la vérité de nos principes. S’il l’était alors on ne pourrait rien connaître avec certitude en mathématiques. Même les théories les plus élémentaires seraient douteuses. Par exemple, il est facile de définir une théorie qui contient toutes les égalités de la forme n + p = q où n, p et q sont des entiers positifs. Que cette théorie ne contient pas 2+2 = 5 peut être prouvé à partir de sa définition. Mais dans cette preuve, on raisonne sur l’ensemble de toutes les égalités qui définit la théorie. Ce serait cependant un absurde excès de rigueur logique d’avoir le moindre doute sur sa validité. Les seuls problèmes que posent cette preuve et d’autres semblables sont d’une part la portée des principes utilisés et d’autre part la façon de les formuler avec précision. Tant qu’on se limite à des techniques élémentaires, on peut être sûr de leur fiabilité, mais qu’en est-il quand on veut étendre leur puissance ?

Avant de définir la moindre théorie axiomatique des ensembles, nous savons qu’il y a des systèmes d’axiomes cohérents pour les ensembles parce que nous savons que les ensembles existent d’une façon idéale. Il y a parfois des doutes sur la justesse d’une théorie particulière. Russell a prouvé que la théorie fregeienne des ensembles est contradictoire. On peut aussi avoir des doutes sur le choix de règles formelles particulières. Des logiciens se sont déjà trompés dans l’énoncé des règles pour les variables, par exemple, en omettant de mentionner des contraintes sur les occurrences libres et liées dans les règles de déduction. Mais il n’y a pas de raison d’être plus sceptique sur l’existence idéale de nombreux ensembles élémentaires que sur l’existence des nombres entiers.

Avant de définir des méthodes formelles, nous savons que certains de nos raisonnements naturels sont fiables, parce que leurs principes sont nécessaires pour tout être rationnel, au sens où toute personne qui prend le temps d’y penser tombe d’accord sur leur nécessité. Si nous n’étions pas convaincus par la vérité de ces principes élémentaires (règles de déduction, vérités sur les mots, les formules et leurs ensembles…) alors nous ne pourrions pas être rationnels. Nous sommes convaincus que certaines preuves ont quelque chose à voir avec la vérité. Avant d’énoncer formellement nos principes, nous savons ou nous croyons qu’ils ont une part de vérité. Pourrions-nous avoir tort ?

Que les principes fondamentaux de la raison soient faux ne pourra jamais être prouvé parce que cette preuve affirmerait qu’il n’y a aucune preuve valide et se contredirait elle-même. Est-ce que cet argument prouve que les principes fondamentaux de la raison contiennent une part de vérité ? Il peut être considéré comme une sorte de confirmation, mais le point important est que la preuve de la fiabilité des principes de preuve n’est pas une étape préliminaire obligatoire pour établir la validité d’une preuve. Cette interprétation du principe de Leibniz conduirait à une régression à l’infini et serait donc absurde. À chaque fois que nous donnons une preuve, nous pouvons supposer une sorte d’accord tacite et préalable sur la validité d’au moins quelques principes de preuve, même s’ils ne sont pas clairement formulés.

Les découvertes scientifiques sont en vérité de bien meilleures preuves de la validité de nos principes de preuve que tout argument a priori.

Tant qu’on se limite aux cas les plus élémentaires, on peut se fier à nos connaissances intuitives sur les principes de preuve. Mais si on veut aller plus loin, alors il faut s’interroger de façon critique sur la fiabilité de nos méthodes et prouver avec des moyens élémentaires que des méthodes non-élémentaires sont fiables. Ce point est développé dans ce chapitre. Il résume à lui seul tout l’esprit de cette approche des fondements des mathématiques. C’est l’histoire du lion, la vérité, qui se fait aider par une souris, les évidences élémentaires.

À quoi servent les méthodes formelles ?

Quand on se limite à des questions élémentaires, on peut être sûr que les preuves informelles sont valides. On n’a pas besoin des méthodes formelles pour s’assurer de l’absolue vérité de ce qu’on dit, les évidences naturelles suffisent. Mais ce n’est qu’un commencement. Les méthodes formelles permettent d’aller beaucoup plus loin, pour plusieurs raisons.

Les façons naturelles de parler et de raisonner marchent bien quand le sujet étudié n’est pas trop compliqué. Quand ce n’est pas le cas, on a besoin de moyens d’expression plus précis que ceux des langues naturelles. Les méthodes formelles permettent de combiner avec justesse des étapes simples, élémentaires, mais qui ensemble permettent de répondre à des questions précises sur des objets très complexes. L’inefficacité des raisonnements courants vient dans ce cas de leur manque de précision.

Les sophismes et les paradoxes montrent que les évidences naturelles peuvent conduire à des absurdités. Les prémisses choisies comme point de départ semblent vraies, ou au moins acceptables, les étapes du raisonnement semblent correctes et pourtant la conclusion est absurde. Dans les sophismes on arrive à reconnaître une sorte de malveillance à l’égard du langage. L’indétermination partielle des significations des notions familières est utilisée pour duper l’auditoire. Typiquement pour faire un sophisme il suffit de se servir du même mot en deux sens différents sans souligner cette nécessaire distinction. Les méthodes formelles permettent de se protéger contre les sophismes parce qu’elles imposent de tout expliciter. La confusion des significations n’est alors plus possible.

Les sophismes n’épuisent pas toutes les absurdités que l’on peut trouver à partir des évidences naturelles. Dans certains cas très importants, le raisonnement qui conduit à une conclusion absurde résiste aux efforts de clarification des significations. Dans ce cas, il s’agit d’un paradoxe. Donnons un exemple. Que toute phrase qui a un sens précis et non-équivoque soit nécessairement ou bien vraie, ou bien non, semble être un principe naturel de la raison. Considérons alors la phrase suivante. Cette phrase est fausse. Elle a un sens précis et non équivoque quand son sujet, « cette phrase » renvoie à la phrase complète. Est-elle vraie ? Si elle était vraie, elle serait fausse. On voudrait en conclure qu’elle n’est pas vraie mais cette option aussi est interdite parce qu’alors elle serait vraie. Elle ne peut donc être ni vraie, ni fausse, contrairement au principe pourtant naturel qui a été précédemment énoncé.

Le paradoxe du menteur, qui vient d’être présenté, est comme beaucoup d’autres paradoxes, très important pour la recherche des vérités. Le chapitre 4 a rappelé son importance dans les preuves d’incomplétude des principes mathématiques.

À la fin du XIX^e siècle, la recherche de principes généraux pour toutes les mathématiques est devenue une question centrale. La théorie des ensembles de Cantor et les progrès de la logique mathématique ont fait espérer une théorie mathématique générale et complète. Il s’agissait de trouver un nombre fini d’axiomes à partir desquels on aurait pu prouver toutes les vérités sur tous les êtres mathématiques concevables. Cependant la théorie de Cantor a des aspects paradoxaux et la fiabilité des raisonnements généraux sur les ensembles laissait une place au doute. Frege, parmi d’autres logiciens a développé des méthodes formelles qui permettaient de formuler avec précision tous les énoncés mathématiques sur les ensembles et tous les axiomes qui semblaient naturels pour fixer la signification des notions fondamentales.

La méthode formaliste de Frege lui a permis d’éviter tous les sophismes, mais il est tombé sur un paradoxe. Russell lui a prouvé que ses axiomes, pourtant naturels, conduisent à une contradiction. Cette preuve a été présentée dans le chapitre 3.

Sans les méthodes formelles, on ne peut pas espérer répondre au problème de la fiabilité ou de la cohérence des principes mathématiques. Il faut être précis, comme Frege, sur ce qu’on prend comme axiomes et sur ce qu’on admet comme règle de déduction, pour pouvoir alors prouver que les principes sont cohérents. On ne peut pas le faire pour les principes naturels parce qu’ils sont incohérents. Bien naïf est celui qui n’a pas compris qu’on peut toujours tout prouver, à la fois une chose et son contraire, il suffit de quelques phrases bien tournées. Mais il n’est souvent pas difficile de se protéger contre cette absurdité de la raison naturelle. Pour les raisonnements courants, il suffit en général de préciser un peu les significations. Si on rencontre un paradoxe, on sait alors qu’on a besoin d’une théorie plus prudente quant au choix de ses principes. On est conduit à développer une théorie formelle avec des axiomes et des règles clairement explicitées.

Le programme de Hilbert

Le paradoxe de Russell, comme de nombreux autres paradoxes ensemblistes, se pose à propos de grands ensembles, tels que l’ensemble de tous les ensembles, l’ensemble de tous les ensembles qui ne sont pas dans eux-mêmes, l’ensemble de tous les ordinaux, et quelques autres. Cette situation avait jeté un soupçon sur les découvertes de Cantor. Certains mathématiciens restaient sceptiques quant à la signification et à la portée de ses théorèmes. Mais d’autres plus audacieux ont compris que Cantor avait livré les clés d’un paradis parce qu’il a donné les moyens de raisonner avec justesse sur tous les ensembles concevables et que cela permettait de développer des théories beaucoup plus puissantes que tout ce qui avait été conçu jusque là.

Les paradoxes de la théorie des ensembles ne remettaient pas en question la vérité des principes élémentaires, tels que ceux des théories des nombres entiers. Tant qu’on se limite aux nombres entiers, l’évidence des principes n’est pas contestable. Les théories sont des ensembles de formules et peuvent être définies avec des principes semblables à ceux qui sont utilisés en arithmétique. Dans les deux cas, on peut raisonner comme si l’on parlait de suites finies de signes graphiques. Hilbert faisait remarquer que les nombres peuvent être identifiés à des suites de barres par exemple : 1=/, 2=//, 3=///, 4=////… Les formules peuvent de même être identifiées à des suites de lettres, ou symboles. Les ensembles de nombres ou de formules sont des systèmes formels. Tant qu’on se limite aux systèmes formels et à quelques autres ensembles que l’on peut construire à partir d’eux, les mathématiques sont finitaires.

On peut formaliser la théorie de Cantor, c’est-à-dire définir avec précision un ensemble de formules prouvables à partir d’axiomes. On obtient ainsi un ensemble finitaire de formules destinées à dire des vérités sur tous les ensembles, et pas seulement ceux qui peuvent être identifiés à des ensembles finitaires déjà construits. Pour développer la théorie générale des ensembles sans tomber dans des contradictions, on est conduit à étudier un ensemble finitaire. On peut alors espérer prouver avec des méthodes finitaires que la théorie est cohérente. Cela place les mathématiques finitaires au cœur de toutes les mathématiques, parce que si on a prouvé qu’une théorie est cohérente on a établi du même coup l’existence mathématique des êtres qu’elle définit. La fiabilité des méthodes générales peut ainsi être prouvée avec des méthodes finitaires.

Hilbert a espéré trouver une théorie finitaire telle que toutes les questions mathématiques y reçoivent une réponse. Cet espoir était justifié en partie, parce que la cohérence de toute théorie est une question finitaire. Gödel a prouvé que ce programme complet de Hilbert n’est pas réalisable. Quelles que soient les théories finitaires que l’on se donne, elles seront toujours insuffisantes pour prouver toutes les vérités. Gödel a aussi prouvé un second théorème d’incomplétude qui a été mal interprété. Il dit qu’en général une théorie mathématique ne peut pas prouver sa propre cohérence. L’interprétation erronée consiste à en conclure que les méthodes finitaires ne suffisent pas pour prouver la cohérence des théories finitaires et qu’il faut abandonner à la fois le programme de Hilbert et la croyance en la prééminence des méthodes élémentaires.

Les sections suivantes prouveront que le programme de Hilbert est réalisable, pourvu qu’on abandonne l’espoir de complétude, qu’on demande seulement des preuves de cohérence, qu’on fasse attention dans le développement de l’ontologie des ensembles et des fonctions, et qu’on fasse confiance à la capacité de la raison à connaître les ensembles infinis, au moins quand ils sont définis avec des moyens élémentaires. Ce programme est considéré ici comme une forme moderne du programme de Leibniz, selon lequel il faut prouver la vérité des principes.

Les preuves de cohérence par la théorie des modèles

On peut prouver la cohérence d’une théorie T en construisant un modèle de T, c’est-à-dire un ensemble de formules atomiques telles que tous les axiomes de T sont vrais pour elles. L’ensemble des vérités atomiques de l’arithmétique élémentaire permet par exemple de prouver la cohérence des théories arithmétiques.

Une théorie T est cohérente lorsqu’on ne peut pas déduire de contradiction à partir de ses axiomes. Si T a un modèle, tous les axiomes et toutes leurs conséquences logiques sont vrais dans ce modèle. Une contradiction est fausse dans tous les modèles. Elle ne peut donc pas être une conséquence des axiomes. Une théorie qui a un modèle est donc nécessairement cohérente. Le théorème de complétude de la logique du premier ordre montre qu’inversement une théorie cohérente a toujours un modèle.

La construction d’un modèle peut être donnée avec un langage et un raisonnement naturels parce qu’elle est souvent très élémentaire. On peut être aussi sûr de la validité de ces constructions qu’on l’est de la validité de tous les principes élémentaires de raisonnement. Il est cependant souhaitable de formaliser les preuves naturelles. Il ne s’agit pas toujours de les rendre plus sûres, parce que certains raisonnements naturels peuvent être plus fiables que les calculs formalisés, étant plus compréhensibles. On peut se tromper dans les options de formalisation, mais, on ne se trompe pas si on applique avec attention des principes élémentaires et naturels sur des questions simples. Formaliser des preuves naturelles présente un intérêt plus pour montrer la justesse et l’efficacité de la formalisation que pour montrer la justesse des preuves elles-mêmes.

Les théories formalisées permettent de dépasser les limites des raisonnements naturels et de formaliser des preuves difficiles. Pour formaliser des preuves de cohérence par la théorie des modèles on a besoin d’une théorie T des ensembles. Pour que ces preuves soient valables, il faut que T soit elle-même cohérente. On est donc conduit à chercher une preuve de la cohérence de T. Nous présenterons à la fin de ce chapitre la preuve de Gödel que sous des conditions générales, une théorie T ne permet pas de formaliser la preuve de la cohérence de T. Nous montrerons que cette improuvabilité a une racine ontologique. T ne contient jamais les bons ensembles qui permettent de formaliser la preuve de sa cohérence.

Nous donnerons d’abord une preuve naturelle de la cohérence de l’arithmétique formelle AF. L’ontologie de l’arithmétique formelle n’est pas adaptée à la formalisation de cette preuve, mais celle de Finitaire1 oui.

Nous montrerons que la théorie Finitaire1 permet de formaliser la preuve naturelle de la cohérence de l’arithmétique formelle. L’ontologie de Finitaire1 est limitée mais elle est cependant très riche. Elle permet de définir beaucoup plus d’ensembles que l’arithmétique formelle, qui est déjà elle-même très riche. Finitaire1 met à profit des méthodes élémentaires et cependant très puissantes et très générales pour construire et connaître des ensembles infinis.

On donnera ensuite une preuve de la cohérence de Finitaire1 et on complétera son ontologie pour définir une théorie Finitaire2 qui permet de formaliser la preuve de la cohérence de Finitaire1.

La preuve de la cohérence de Finitaire2 sera laissée en exercice, mais arrivé à ce point le lecteur devrait être convaincu qu’elle ne pose pas de difficultés de principe. Il suffit de se donner une ontologie adaptée à ce but.

La méthode qui vient d’être exposée rencontre l’objection suivante. On prouve la cohérence d’une théorie T avec une théorie T+ plus compliquée que T. Il se pourrait que T soit incohérente, que T+ le soit également et qu’elle permette quand même de prouver que T est cohérente. Ces preuves de cohérence ne prouveraient donc rien du tout.

Cette objection n’est ici pas valable. Avant de définir Finitaire1, on sait déjà que l’arithmétique formelle est cohérente et on sait le prouver. Le rôle de Finitaire1 est seulement de traduire une preuve naturelle dans un langage formalisé. Si ses axiomes avaient été mal choisis, Finitaire1 pourrait être incohérente, mais cela n’enlèverait rien à la valeur de la preuve de la cohérence de l’arithmétique formelle, cela montrerait seulement les difficultés de la formalisation des preuves naturelles.

Comme on sait que Finitaire1 et d’autres théories finitaires élargies sont cohérentes, on peut s’en servir pour prouver la cohérence d’autres théories. Nous prouverons que les méthodes finitaires sont en un sens toujours suffisantes, au sens où si une théorie est cohérente alors elle a un modèle finitaire. C’est une conséquence, ou plus exactement une reformulation, du théorème de complétude de Gödel. Mais on ne peut pas déduire de ce théorème l’existence d’une théorie finitaire complète, au sens où elle suffirait pour toutes les preuves de cohérence.

Les preuves formelles de cohérence sont assez élémentaires. Il suffit de définir avec précision à la fois un modèle et l’ensemble des axiomes de la théorie, et d’appliquer quelques règles logiques simples. Le théorème de cohérence est une conséquence triviale des définitions. C’est en accord avec l’intuition que ces théories sont évidemment cohérentes. La trivialité de la conclusion veut quand même dire ici qu’il faudrait y passer quelques dizaines de pages si l’on voulait expliciter formellement toutes les étapes. Mais la rédaction complète de ces preuves formelles ne pose pas d’autres difficultés que le caractère mécanique et répétitif de leurs nombreuses étapes. Même pour une théorie aussi élémentaire que celle des nombres entiers, la construction d’un modèle est assez compliquée, mais elle ne met en jeu que des étapes élémentaires, pour lesquelles la validité des méthodes de construction est difficilement contestable, sauf si l’on prétend que l’esprit humain est incapable de connaître les nombres entiers.

La seule véritable difficulté de ces preuves formelles consiste à choisir une ontologie adaptée à leur but.