Dictionnaire de philosophie/Démonstration

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

※ Démonstration ※

46 pages, 58 min

Euclide (ou Archimède) traçant une figure au compas devant ses élèves, détail de L'École d'Athènes de Raphaël (1509-1511). Démontrer, au sens premier, c'est faire voir.

Une démonstration (du latin demonstratio, « action de montrer, de faire voir », dérivé de monstrare ; les Grecs disaient apodeixis, ἀπόδειξις, formé sur deiknumi, « montrer ») est un raisonnement qui établit la vérité d'une proposition en la faisant dériver, par une suite d'inférences réglées, de propositions déjà admises. La langue courante a gardé la racine : on fait la démonstration d'un appareil, on assiste à une démonstration de force, on multiplie les démonstrations d'affection. Dans tous ces emplois, démontrer, c'est rendre visible. Le sens philosophique et mathématique du mot conserve cette parenté, mais la déplace : ce que la démonstration donne à voir n'est plus une chose, c'est une nécessité. Quand nous avons suivi la preuve du théorème de Pythagore, nous ne savons pas seulement que le carré de l'hypoténuse égale la somme des carrés des deux autres côtés ; nous voyons que cela ne peut pas être autrement, et pourquoi.

Cette prétention distingue la démonstration de ses voisines. La preuve expérimentale établit des faits, des régularités, des lois même ; mais ce qu'elle établit demeure faillible et révisable, et aurait pu, pour autant que la logique en décide, être autre ; le témoignage rapporte, l'indice suggère, la statistique rend probable. L'argumentation, elle, cherche à convaincre un auditoire, avec plus ou moins de succès selon les personnes et les circonstances. La démonstration prétend contraindre : quiconque accorde les prémisses et comprend les règles doit accorder la conclusion, qu'il le veuille ou non. En français, « preuve » et « démonstration » s'emploient souvent l'un pour l'autre chez les mathématiciens ; mais « preuve » couvre un champ plus vaste (preuve judiciaire, preuve d'amour, charge de la preuve), tandis que « démonstration » désigne au sens strict la preuve déductive, celle qui enchaîne des raisons.

Trois questions traversent l'histoire de la notion, et cet article avec elle. D'où partent les démonstrations, puisqu'on ne peut pas tout démontrer sans régresser à l'infini ? Que garantissent-elles au juste : la vérité de la conclusion, sa nécessité, ou seulement sa dépendance à l'égard des prémisses ? Et qu'exigent-elles de celui qui les suit : une vision, un calcul, une adhésion ? Née dans la géométrie grecque, théorisée par Aristote, érigée en idéal de la raison à l'âge classique, la démonstration a connu au XIX^e siècle et au XX^e siècle une double aventure : elle a perdu son socle d'évidences avec les géométries non euclidiennes, puis elle est devenue elle-même un objet d'étude mathématique, au point qu'une discipline entière porte aujourd'hui son nom, la théorie de la démonstration. En chemin, elle a rencontré ses limites, de Gödel aux ordinateurs, et n'a cessé de poser à la philosophie une question embarrassante : la philosophie elle-même démontre-t-elle quoi que ce soit ?

Pour le lecteur pressé, voici l'histoire en raccourci. Les Grecs inventent la preuve ; Aristote en fait la théorie, Euclide le modèle. Le Moyen Âge la transmet et l'affine, de Bagdad à Paris. L'âge classique en fait l'idéal de toute connaissance ; Kant la réserve aux mathématiques. Le XIX^e siècle découvre que ses axiomes ne sont pas des évidences ; Frege et Hilbert la formalisent, jusqu'à en faire un objet mathématique ; Gödel démontre qu'aucun système cohérent n'épuise la vérité arithmétique. La logique contemporaine étudie cet objet comme une structure, découvre qu'une preuve est un programme, et la confie aux machines. La philosophie, pendant ce temps, se demande si elle-même a jamais rien démontré. Le détail suit.

Aux origines : l'invention grecque de la preuve

Des recettes aux raisons

Les mathématiques n'ont pas commencé avec la démonstration. Les scribes de Babylone et d'Égypte savaient résoudre des équations du second degré, calculer des volumes, arpenter des champs ; les tablettes et les papyrus qui nous sont parvenus contiennent des procédures, des exemples résolus, parfois des vérifications sur des cas particuliers. Ce qui manque, ce n'est pas l'exactitude, c'est un certain type de discours : les documents conservés ne témoignent nulle part de l'exigence de faire découler un résultat général de principes explicites, par un raisonnement que chacun puisse contrôler pas à pas. L'invention grecque, entre le VI^e siècle et le IV^e siècle avant notre ère, n'est donc pas d'abord une invention de contenus : c'est l'invention d'une norme. La tradition, transmise par Proclus d'après l'historien Eudème, en attribue les premiers gestes à Thalès de Milet, qui aurait démontré que le diamètre partage le cercle en deux parties égales ou que les angles à la base d'un triangle isocèle sont égaux : des énoncés que tout arpenteur tenait pour acquis, mais que personne, avant lui, n'avait songé à établir.

Pourquoi établir ce que tout le monde voit ? Un exemple, le plus célèbre de l'Antiquité, fait comprendre ce que la démonstration apporte que l'expérience ne donnera jamais. Prenons un carré de côté 1 et demandons la longueur de sa diagonale. Aucune mesure, si fine soit-elle, ne tranchera la question de savoir si cette longueur peut s'écrire comme un rapport de deux entiers. Les Pythagoriciens, sans doute vers la fin du V^e siècle avant notre ère, ont démontré que non : supposons que la diagonale et le côté soient commensurables, c'est-à-dire que leur rapport s'écrive p/q sous forme irréductible ; le théorème de Pythagore donne p² = 2q², donc p est pair, donc p² est divisible par 4, donc q² est pair, donc q est pair ; p et q seraient alors tous deux pairs, ce qui contredit l'irréductibilité de la fraction. La supposition s'effondre sous sa propre conséquence. Aristote cite ce raisonnement comme exemple type de la déduction qui conclut « par l'impossible ». Sa portée est immense : la démonstration vient d'atteindre un ordre de faits auquel nulle observation n'accédera, l'impossibilité. On ne constate pas qu'une chose ne peut pas être ; on le démontre.

Cette exigence nouvelle a un contexte. La cité grecque est une culture de la parole publique et de la contestation : au tribunal comme à l'assemblée, chacun doit rendre raison de ce qu'il avance devant des égaux qui peuvent le contredire. Des historiens des sciences ont vu dans cette pratique agonistique du débat l'un des terreaux de la preuve mathématique, qui pousse la reddition de comptes jusqu'à son point extrême : un discours construit pour qu'aucune objection ne reste possible. La philosophie naissante fournit l'autre versant : le poème de Parménide déduit les caractères de l'être à partir de la seule impossibilité du non-être, et les paradoxes de Zénon d'Élée réfutent le mouvement en tirant de sa supposition des conséquences inacceptables. Sans être des démonstrations au sens mathématique, ces raisonnements en répandent le style : poser, déduire, réfuter. Le mot même de démonstration s'installera dans ce paysage où l'on prouve contre un adversaire, réel ou possible.

Platon : la géométrie sous la dialectique

Platon a fait de la géométrie l'antichambre de la philosophie ; l'Académie, si l'on en croit une tradition tardive et d'historicité douteuse, mais parlante, en aurait refusé l'entrée à qui l'ignorait. Le Ménon contient l'une des plus anciennes scènes de démonstration de la littérature philosophique : Socrate interroge un jeune esclave qui n'a jamais étudié, et lui fait trouver, figure à l'appui, comment construire un carré d'aire double d'un carré donné. L'esclave commence par répondre ce que répondrait chacun de nous : il suffit de doubler le côté. Socrate lui fait dessiner la figure ; l'esclave voit que le carré obtenu est quadruple, non double ; il essaie un côté de longueur intermédiaire, échoue encore, avoue son embarras. C'est alors, une fois l'évidence première détruite, que le questionnement le conduit à la solution : le carré construit sur la diagonale. La démonstration apparaît ici sous son double visage : elle réfute d'abord ce que nous croyions voir, elle fait voir ensuite ce que nous ne soupçonnions pas. Platon en tire sa thèse de la réminiscence ; on peut, plus sobrement, y lire que démontrer n'est pas transmettre un contenu, mais conduire un esprit à produire lui-même la nécessité d'une conclusion.

Pourtant Platon refuse de faire de la démonstration géométrique le modèle suprême du savoir. Dans la République, l'image de la ligne assigne aux mathématiques une place intermédiaire : le géomètre part d'hypothèses, le pair et l'impair, les figures, les trois espèces d'angles, qu'il traite comme évidentes et dont il ne rend pas raison ; il descend de ces hypothèses vers leurs conséquences, sans jamais remonter vers un principe qui les fonderait. La dialectique, elle, prend les hypothèses pour ce qu'elles sont, des points d'appui provisoires, et s'élève de proche en proche jusqu'à un principe anhypothétique ; au livre VII, Platon dit qu'elle « détruit les hypothèses », c'est-à-dire qu'elle les prive de leur statut de points de départ absolus pour les fonder ou les dépasser. Le geste est lourd de conséquences : il inaugure la question, qui ne quittera plus la philosophie, du fondement des démonstrations. Une chaîne déductive vaut ce que valent ses premiers anneaux ; qui garantit les premiers anneaux ? Platon répond : un savoir d'un autre type, dialectique et non déductif. Aristote répondra autrement.

Aristote : la théorie du savoir démonstratif

Avec les Seconds Analytiques, la démonstration cesse d'être une pratique pour devenir un objet de théorie. Aristote y définit la science (epistêmê) par la démonstration : savoir scientifiquement, c'est connaître la cause par laquelle la chose est, savoir qu'elle est la cause de la chose, et que la chose ne peut pas être autrement. L'instrument de ce savoir est ce qu'il appelle « le syllogisme scientifique » : un raisonnement en forme dont les prémisses doivent satisfaire des conditions strictes. Elles doivent être vraies (on ne fonde pas un savoir sur le faux), premières et immédiates (sinon elles demanderaient elles-mêmes démonstration), plus connues que la conclusion, antérieures à elle, et causes d'elle. Cette dernière exigence est la plus forte : la démonstration aristotélicienne ne se contente pas d'établir « que » (hoti), elle doit livrer le « pourquoi » (dioti). Aristote illustre la différence par un exemple d'astronomie : des planètes, on peut conclure qu'elles sont proches parce qu'elles ne scintillent pas ; le raisonnement est correct, mais il va de l'effet à la cause. La démonstration digne de ce nom suit le sens inverse : les planètes ne scintillent pas parce qu'elles sont proches, et c'est la proximité, cause réelle, qui doit servir de moyen terme. Démontrer, c'est ordonner le savoir selon l'ordre des choses.

Restait à affronter la difficulté que Platon avait léguée. Si tout savoir vient par démonstration, les prémisses de chaque démonstration doivent être sues, donc démontrées, et ainsi sans fin : la régression à l'infini rend le savoir impossible. Si, pour l'éviter, on accepte que les prémisses soient démontrées à partir de la conclusion, on tombe dans le cercle, qui ne vaut pas mieux ; les sceptiques feront plus tard de ce dilemme, régression, cercle ou arrêt arbitraire, une machine de guerre contre toute prétention au savoir, connue sous le nom de trilemme d'Agrippe ou de diallèle. La réponse d'Aristote tient en une thèse : tout savoir n'est pas démonstratif. Il existe des principes indémontrables, axiomes communs à toutes les sciences, définitions et hypothèses propres à chacune, et la connaissance de ces principes relève d'une autre faculté que la science déductive : l'intellect (noûs), qui les saisit au terme d'une induction prenant appui sur l'expérience répétée. La démonstration ne se fonde pas elle-même ; elle repose sur un acte de saisie qui n'est plus de l'ordre de la preuve. Toute la postérité de la notion se jouera dans l'écart entre ces deux moments : l'enchaînement, que l'on peut régler, et le point de départ, qu'il faut voir.

Aristote assortit sa théorie de deux thèses qui feront date. La première concerne le principe de non-contradiction : principe de tous les principes, il ne peut être démontré, puisque toute démonstration le présuppose ; mais on peut le défendre « par réfutation », en montrant que quiconque le conteste doit, pour le contester, parler, donc signifier quelque chose de déterminé, donc s'y soumettre déjà. Cette démonstration réfutative, qui retourne contre l'adversaire l'acte même de son objection, restera un modèle pour les philosophes en quête de preuves indirectes. La seconde thèse cloisonne les sciences : chaque genre a ses principes propres, et il est interdit de « passer d'un genre à l'autre », de démontrer une vérité géométrique par l'arithmétique par exemple. L'histoire se chargera d'ironiser : la géométrie analytique de Descartes, puis l'arithmétisation de l'analyse au XIX^e siècle, feront précisément ce qu'Aristote interdisait, et y gagneront une puissance démonstrative que le Stagirite ne pouvait imaginer.

De cette théorie, la logique a retenu un partage qu'il vaut la peine de fixer dès maintenant, car tout ce qui suit le suppose. Une inférence est dite valide quand sa forme interdit que les prémisses soient vraies et la conclusion fausse : la vérité, si elle entre, ne peut plus sortir. La validité ne garantit donc rien quant aux faits ; un raisonnement de forme irréprochable conclut le faux de prémisses fausses, et « tous les chats sont des oiseaux, or tout oiseau vole, donc tous les chats volent » est un modèle de validité. Pour qu'il y ait démonstration au sens plein, il faut deux choses : que chaque pas soit valide, et que les points de départ soient vrais, ou du moins admis ; les logiciens disent alors que le raisonnement est correct. Toute l'architecture aristotélicienne tient dans ce doublet : la syllogistique règle la validité des pas, la théorie des principes répond de la vérité des départs. La logique moderne y ajoutera une troisième distinction, que nous retrouverons au moment voulu : celle de la démontrabilité, propriété d'un énoncé qu'on peut atteindre par les règles d'un système, et de la conséquence, relation sémantique qui tient à la vérité dans toutes les interprétations ; savoir si ces deux notions coïncident deviendra, au XX^e siècle, une question de théorèmes.

Euclide : un modèle pour vingt siècles

L'un des plus anciens témoins des Éléments d'Euclide : fragment de papyrus trouvé à Oxyrhynque (Égypte), copié autour de l'an 100 de notre ère, avec le diagramme de la proposition II, 5.

Vers 300 avant notre ère, Euclide compose à Alexandrie les Éléments, qui donnent à l'idéal aristotélicien son incarnation la plus durable. L'ouvrage s'ouvre sur des définitions (« le point est ce qui n'a aucune partie »), cinq demandes ou postulats (par deux points passe une droite, etc.) et des notions communes (« les grandeurs égales à une même grandeur sont égales entre elles ») ; tout le reste, quatre cent soixante-cinq propositions réparties en treize livres, s'en déduit. Chaque proposition suit un protocole quasi rituel : énoncé général, exposition sur une figure lettrée, construction, démonstration proprement dite, conclusion qui reprend l'énoncé et se clôt par la formule hoper edei deixai, « ce qu'il fallait démontrer », que le latin rendra par quod erat demonstrandum et dont nos copies de collège gardent l'abréviation : CQFD.

Un exemple donne la saveur de cette écriture. À la proposition 20 du livre IX, Euclide établit que « les nombres premiers sont plus nombreux que toute multitude proposée de nombres premiers » : autrement dit, la liste des nombres premiers ne s'achève jamais. Qu'on en propose une collection finie quelconque ; formons le produit de tous ces nombres et ajoutons 1 ; le nombre obtenu n'est divisible par aucun des nombres de la liste, puisqu'il laisse chaque fois le reste 1 ; ou bien il est premier, ou bien il admet un diviseur premier ; dans les deux cas, il existe un nombre premier étranger à la liste. En cinq lignes, l'infini est atteint depuis le fini : nulle énumération n'aurait pu l'établir, et l'on comprend que les mathématiciens citent encore cette page comme un modèle d'élégance. Le théorème de Pythagore, proposition 47 du livre I, reçoit le même traitement : non pas une vérification sur des triangles particuliers, mais une construction qui vaut pour tous les triangles rectangles possibles.

Pendant plus de deux millénaires, les Éléments ont défini ce que démontrer veut dire ; l'expression more geometrico, « à la manière des géomètres », désignera l'idéal de tout savoir bien conduit. Le livre fut un des plus copiés, puis des plus imprimés de la tradition occidentale, et servit de manuel jusqu'au XIX^e siècle. Sa perfection même abritait pourtant deux fragilités, que le temps allait révéler. La première est logique : les démonstrations d'Euclide s'appuient tacitement sur la figure, et supposent des propriétés (qu'une droite coupant un côté d'un triangle en ressort, par exemple) qu'aucun postulat n'énonce ; la rigueur euclidienne, réexaminée à l'époque moderne, se révélera trouée d'appels à l'intuition. La seconde tient au cinquième postulat, celui des parallèles, si peu évident en comparaison des autres qu'Euclide lui-même retarde son emploi jusqu'à la proposition 29 : des générations de géomètres tenteront de le démontrer à partir des quatre premiers, et leur échec, on le verra, changera le sens même du mot démonstration.

Le Moyen Âge : demonstratio et burhān

De Bagdad à Paris : le retour des Analytiques

Entre Euclide et Descartes, l'idéal démonstratif ne dort pas : il voyage. De l'Organon d'Aristote, le haut Moyen Âge latin ne lit guère que les Catégories et le traité De l'interprétation, transmis par Boèce ; les Seconds Analytiques, c'est-à-dire la théorie même de la démonstration, manquent à l'appel, et la scientia n'est connue que de seconde main. C'est en terre d'islam que le texte trouve d'abord ses lecteurs : traduit en arabe au début du X^e siècle par Abū Bishr Mattā, dans le sillage des grandes entreprises de traduction de Bagdad, il y reçoit le nom qui désignera toute la discipline, burhān, la démonstration. Al-Fārābī, au X^e siècle, en tire une hiérarchie des discours qui fera fortune : cinq arts se partagent le langage, démonstratif, dialectique, sophistique, rhétorique et poétique, et seul le premier engendre l'assentiment certain ; les autres persuadent, ébranlent ou charment, à des degrés d'assurance décroissants. Avicenne consacre à la démonstration un livre entier de son encyclopédie, le Kitāb al-Shifā, où les conditions aristotéliciennes du savoir certain sont réélaborées. Averroès, enfin, ne se contente pas de commenter les Seconds Analytiques ligne à ligne : dans le Faṣl al-maqāl (vers 1179), une épître de droit religieux dont le titre annonce qu'elle tranche la question, il distingue trois classes d'hommes selon le mode d'assentiment dont ils sont capables, les gens de démonstration, les gens de dialectique et les gens de rhétorique ; le texte révélé s'adresse aux trois à la fois, mais son interprétation savante (ta'wīl) revient de droit aux seuls démonstratifs, c'est-à-dire aux philosophes. Il fallait oser : un juriste y établit, en forme de consultation légale, que la démonstration est pour certains hommes une obligation. Le latin rattrape son retard au XII^e siècle : Jacques de Venise traduit les Seconds Analytiques depuis le grec vers 1130, Gérard de Crémone depuis l'arabe quelques décennies plus tard, et cette logica nova entre dans les universités naissantes ; Robert Grosseteste, vers 1230, en donne le premier grand commentaire latin. Pendant trois siècles, la démonstration sera au programme de tout étudiant d'Occident.

La scientia des docteurs

La scolastique reçoit ainsi d'Aristote un mot exigeant, scientia : n'est su, au sens strict, que ce qui est démontré depuis des principes par sa cause. Elle en affine l'outillage. Le couple que nous avons rencontré chez Aristote, conclure « que » ou conclure « pourquoi », devient la distinction canonique de la demonstratio quia, qui remonte de l'effet à la cause, et de la demonstratio propter quid, qui descend de la cause à l'effet, seule démonstration parfaite. Thomas d'Aquin s'en sert pour répondre à une question que nul Grec ne s'était posée dans ces termes : la théologie est-elle une science ? Oui, répond-il, mais une science subalternée : de même que l'optique emprunte ses principes à la géométrie et la musique à l'arithmétique, sans les redémontrer, la doctrine sacrée reçoit les siens d'une science plus haute, celle que Dieu et les bienheureux possèdent, et raisonne démonstrativement à partir d'articles qu'elle tient de la révélation. Quant à l'existence de Dieu elle-même, Thomas refuse d'un même geste deux facilités. Elle n'est pas évidente pour nous, et la preuve purement conceptuelle qu'Anselme de Cantorbéry avait proposée au XI^e siècle, tirant l'existence de la seule notion de « ce dont rien de plus grand ne peut être pensé » (id quo maius cogitari nequit), ne conclut pas ; mais elle n'est pas non plus indémontrable : une demonstratio quia, partant des effets sensibles, peut remonter jusqu'à leur cause première, et c'est ce que font les cinq voies. Le lecteur retrouvera ce geste : quand Kant défera la preuve ontologique sous sa forme cartésienne, il répétera, dans un autre paysage, le refus thomasien de tirer l'existence d'un concept.

La fin du Moyen Âge resserre l'étau. Guillaume d'Ockham, au XIV^e siècle, maintient la définition stricte de la démonstration mais en réduit le domaine d'application : hors des mathématiques, bien peu de nos savoirs satisfont aux conditions du propter quid. Sur Dieu même, la démonstration recule : qu'il existe une cause première, on peut l'établir ; qu'elle soit unique, ou infinie, excède selon lui les forces de la raison démonstrative, et relève de la foi. Un monde créé par une toute-puissance libre est un monde où les liaisons entre les choses auraient pu être autres : la nécessité s'y fait rare, et avec elle la démonstration au sens fort. Ce resserrement nominaliste lègue à la modernité un partage durable entre ce qui se démontre et ce qui se croit, en même temps qu'une inquiétude sur les preuves en matière naturelle. Quand Descartes, trois siècles plus tard, congédiera le syllogisme des écoles au motif qu'il sert à exposer ce qu'on sait déjà plutôt qu'à trouver du neuf, c'est de cette scientia scolastique, reçue et discutée pendant trois cents ans, qu'il héritera en s'en détachant.

L'âge classique : la raison démonstrative

Descartes : l'ordre des raisons

Le XVII^e siècle porte l'idéal démonstratif à son plus haut degré d'ambition : ce que la géométrie a fait pour les figures, la philosophie le fera pour l'ensemble du savoir. Descartes donne le ton dans le Discours de la méthode : « Ces longues chaînes de raisons, toutes simples et faciles, dont les géomètres ont coutume de se servir pour parvenir à leurs plus difficiles démonstrations, m'avaient donné occasion de m'imaginer que toutes les choses qui peuvent tomber sous la connaissance des hommes s'entresuivent en même façon ». L'image de la chaîne dit l'essentiel de sa conception : une démonstration vaut par la solidité de chaque maillon et par la continuité de leur enchaînement. Les Règles pour la direction de l'esprit en donnent la théorie : la connaissance certaine repose sur deux opérations, l'intuition, saisie immédiate d'un esprit pur et attentif qui voit une vérité simple sans pouvoir en douter, et la déduction, qui n'est rien d'autre qu'une suite d'intuitions, chaque passage d'un anneau au suivant étant lui-même vu avec évidence. La déduction cartésienne n'est donc pas un mécanisme formel : elle est une vision prolongée, que la mémoire relaie quand la chaîne s'allonge, et que l'énumération, recommandée par la règle VII, vient sécuriser en reparcourant d'un mouvement continu la suite entière des raisons.

Cette primauté de l'intuition explique une thèse célèbre. Aux objections qui voyaient dans le cogito un syllogisme tronqué (tout ce qui pense existe ; or je pense ; donc je suis), Descartes répond que celui qui dit « je pense, donc je suis » ne conclut pas son existence de sa pensée « comme par la force de quelque syllogisme », mais la voit « par une simple inspection de l'esprit ». La première certitude n'est pas démontrée : elle est éprouvée. Il y a là plus qu'une coquetterie d'auteur ; c'est la reprise, en régime moderne, de la thèse d'Aristote selon laquelle les commencements ne relèvent pas de la preuve. Descartes en tire une distinction de méthode restée classique, entre l'analyse et la synthèse. La synthèse, dont Euclide est le modèle, part des principes et descend vers les conséquences : elle contraint l'assentiment, mais cache le chemin par lequel on a trouvé. L'analyse suit au contraire « la vraie voie » de la découverte, en remontant du problème vers ses conditions ; c'est elle que suivent les Méditations. Descartes consent pourtant, à la demande de Mersenne, à redisposer ses preuves de l'existence de Dieu et de la distinction de l'âme et du corps « d'une façon géométrique », avec définitions, demandes et axiomes : l'appendice, un peu raide, montre à la fois le prestige du modèle euclidien et la conviction cartésienne qu'il convient mieux à l'exposition qu'à l'invention.

Un dernier trait mérite l'attention, car il paraîtra étrange au lecteur moderne : chez Descartes, la fiabilité des longues démonstrations dépend en dernier ressort de Dieu. Tant que je contemple une vérité simple, je ne puis en douter ; mais sitôt que la chaîne excède ce que je peux embrasser d'un seul regard, je dois me fier à ma mémoire, et au souvenir d'avoir démontré ; or ce crédit suppose que mon auteur ne soit pas trompeur. C'est pourquoi, répond Descartes à ses objecteurs, un géomètre athée peut bien connaître clairement que les trois angles d'un triangle valent deux droits, mais sa connaissance n'est pas une science parfaite, puisqu'un doute peut toujours revenir sur elle. La démonstration, acte humain étendu dans le temps, requiert une garantie qui la dépasse ; on retrouvera cette inquiétude, sécularisée, dans les débats contemporains sur la vérification des preuves longues.

Pascal : grandeur et limites de l'esprit de géométrie

Nul n'a mieux décrit que Pascal, géomètre de génie, ce que la démonstration peut, et ce qu'elle ne peut pas. L'opuscule De l'esprit géométrique commence par rêver la méthode parfaite : elle consisterait « à tout définir et à tout prouver ». Rêve aussitôt congédié : cette méthode est « impossible », car toute définition emploie des mots, qu'il faudrait définir à leur tour, et toute preuve part de propositions, qu'il faudrait prouver ; la régression est sans fin. « Ce qui passe la géométrie nous surpasse ». Mais l'impossibilité de l'idéal ne condamne pas au désordre : entre tout démontrer et ne rien démontrer, il y a la voie de la géométrie effective. « Cet ordre, le plus parfait entre les hommes, consiste non pas à tout définir ou à tout démontrer, ni aussi à ne rien définir ou à ne rien démontrer, mais à se tenir dans ce milieu » : ne pas définir les termes que tous entendent (espace, temps, mouvement, nombre), ne pas prouver les principes que la lumière naturelle donne, et définir et prouver tout le reste. La géométrie ne définit pas tout ni ne prouve tout ; mais, ajoute Pascal, elle ne suppose que des choses claires et constantes par la lumière naturelle, et c'est pourquoi elle est parfaitement sûre : la nature soutient le discours là où le discours défaille.

Les Pensées donnent à cette analyse son cadre anthropologique. « Nous connaissons la vérité non seulement par la raison, mais encore par le cœur ; c'est de cette dernière sorte que nous connaissons les premiers principes ». Le cœur sent qu'il y a trois dimensions dans l'espace et que les nombres sont infinis ; la raison démontre ensuite, en s'appuyant sur ces certitudes senties, qu'il n'y a point deux nombres carrés dont l'un soit double de l'autre. D'où la formule qui résume tout : « Les principes se sentent, les propositions se concluent ». Loin d'humilier la démonstration, ce partage la sauve : exiger d'elle qu'elle prouve ses propres principes, c'est lui demander ce que nulle procédure ne peut donner, et le scepticisme n'a beau jeu que contre cette exigence déplacée. Pascal ajoute une seconde limite, interne celle-là : il est des matières où la démonstration n'a pas prise, non que la vérité y manque, mais parce que les principes y sont trop nombreux et trop déliés pour être ordonnés en chaînes. C'est le partage fameux de l'esprit de géométrie et de l'esprit de finesse : le premier manie des principes « gros et visibles », le second des principes si fins qu'il faut les voir tous d'un seul regard, sans pouvoir les exposer par ordre. Le jugement, la morale, la connaissance des hommes relèvent de la finesse : on n'y démontre pas, on y discerne.

Restait à tirer la conséquence pour l'art de convaincre. La seconde partie de l'opuscule, De l'art de persuader, l'énonce avec une lucidité désenchantée : les hommes n'entrent dans les vérités que par deux portes, l'entendement et la volonté, et la plus fréquentée n'est pas celle du géomètre. Aussi « l'art de persuader consiste autant en celui d'agréer qu'en celui de convaincre ». La démonstration contraint l'entendement ; elle ne gagne pas les cœurs. Trois siècles avant les théoriciens contemporains de l'argumentation, Pascal a marqué la frontière : démontrer et persuader sont deux arts, et le second ne se réduit pas au premier.

Spinoza : une éthique démontrée

L'audace inverse appartient à Spinoza : puisque la démonstration est la forme même du savoir, il faut l'étendre à ce qui semble lui résister le plus, les passions et la conduite humaines. L'Éthique, publiée en 1677, s'intitule en toutes lettres Ethica ordine geometrico demonstrata, éthique démontrée selon l'ordre géométrique : définitions, axiomes, propositions suivies de leurs démonstrations closes par le sigle CQFD, corollaires et scolies s'y enchaînent comme dans Euclide. Le choix n'est pas un ornement. Ceux qui traitent des affects, écrit Spinoza en tête de la troisième partie, préfèrent les maudire ou les railler que les comprendre, comme si l'homme était dans la nature « un empire dans un empire » ; lui entend au contraire considérer « les actions et les appétits humains comme s'il était question de lignes, de surfaces et de solides ». La haine, la jalousie, l'ambition ont des causes et suivent des lois ; les démontrer, c'est cesser d'en être le jouet pour en devenir le connaisseur. La forme géométrique est ici une ascèse : elle interdit l'éloquence, la déploration, l'appel aux préjugés du lecteur, et ne laisse subsister que l'enchaînement des raisons ; les scolies, où Spinoza reprend la parole en son nom, ménagent seuls une respiration dans l'appareil démonstratif.

On a beaucoup discuté pour savoir si cet ordre géométrique est l'essence de la doctrine ou son vêtement d'exposition, et si des définitions initiales peuvent porter tout l'édifice sans être elles-mêmes justifiées. Quoi qu'il en soit du débat entre commentateurs, Spinoza a laissé sur la démonstration une formule que sa hardiesse a rendue célèbre : « les yeux de l'Âme, par lesquels elle voit et observe les choses, sont les démonstrations elles-mêmes ». Démontrer n'est pas, pour l'esprit, un détour laborieux vers ce qu'une vision livrerait mieux : c'est sa manière propre de voir. La formule renverse l'ancienne hiérarchie de l'intuition et du discours ; elle annonce, à sa façon, l'idée moderne que la preuve n'est pas un pis-aller de l'évidence, mais un mode d'accès à des vérités qu'aucune évidence immédiate ne donnerait.

Leibniz : démontrer, c'est calculer

Leibniz porte l'idéal démonstratif sur un autre terrain en le confiant à une autre puissance que la vision : le calcul. Sa théorie repose sur un partage fameux, exposé dans la Monadologie : « Il y a aussi deux sortes de vérités, celles de Raisonnement et celles de Fait ». Les vérités de raisonnement sont nécessaires, et leur opposé est impossible ; on en trouve la raison par l'analyse, en les résolvant « en idées et en vérités plus simples, jusqu'à ce qu'on vienne aux primitives », ces énoncés identiques dont l'opposé enferme une contradiction expresse et qui ne peuvent ni ne doivent être prouvés. Démontrer une vérité nécessaire, c'est donc la réduire, par une chaîne de définitions et de substitutions d'équivalents, à une identité de la forme A est A. Les Nouveaux essais sur l'entendement humain en donnent un exemple resté fameux par sa modestie apparente : la preuve que deux et deux font quatre. Ce n'est pas, dit Leibniz, une vérité immédiate ; posons les définitions (2 est 1 et 1 ; 3 est 2 et 1 ; 4 est 3 et 1) et l'axiome de substitution des égaux ; alors 2 et 2 est 2 et 1 et 1, qui est 3 et 1, qui est 4. Frege remarquera, deux siècles plus tard, que la chaîne comporte encore une lacune, l'associativité de l'addition y étant employée sans être énoncée ; l'anecdote dit assez que l'idéal de la preuve sans reste est plus exigeant que ses meilleurs champions ne l'imaginaient.

De ce que démontrer est analyser, Leibniz tire un rêve qui enjambe les siècles. Si l'on disposait d'une écriture où chaque idée simple aurait son caractère propre, une characteristica universalis, et de règles pour combiner ces caractères, un calculus ratiocinator, alors raisonner deviendrait calculer, et les controverses se videraient comme des erreurs de compte : entre deux philosophes en désaccord, il suffirait de dire « calculons ! » (calculemus) pour voir qui a raison. Le rêve leibnizien déplace le centre de gravité de la démonstration : sa validité ne tiendrait plus à l'évidence que chaque pas procure à un esprit attentif, mais à la correction mécanique de manipulations de signes, contrôlable par n'importe qui, et pourquoi pas par une machine. Il faudra deux siècles pour que Frege commence à honorer ce programme, et un troisième pour que des machines s'y emploient ; mais l'idée était là, et avec elle une question que Descartes n'aurait pas comprise : une démonstration doit-elle être vue, ou seulement vérifiée ?

Un mot enfin du principe qui gouverne chez Leibniz l'autre moitié du savoir. Les vérités de fait, contingentes, ont aussi leur raison, en vertu du grand principe « qu'aucun fait ne saurait se trouver vrai ou existant [...] sans qu'il y ait une raison suffisante pourquoi il en soit ainsi et non pas autrement » ; mais leur analyse va à l'infini, et Dieu seul en embrasse la résolution. L'exigence démonstrative s'étend ainsi, en droit, à la totalité du réel ; simplement, pour les esprits finis, la démonstration des contingents demeure un horizon, non une possession. Peu de thèses auront autant fait pour installer l'idée que tout ce qui est vrai doit pouvoir, en principe, se prouver ; on mesurera plus loin ce que le XX^e siècle a fait de cette équation de la vérité et de la démontrabilité.

Kant : ce que la philosophie ne peut pas démontrer

Au moment où l'idéal du more geometrico triomphe dans les écoles, Kant lui oppose la plus ferme des fins de non-recevoir : la philosophie qui singe la géométrie se paie de mots, car la démonstration au sens strict n'existe qu'en mathématiques. La thèse, exposée dans la « Discipline de la raison pure » qui clôt la Critique de la raison pure, repose sur une analyse de ce qui rend la preuve mathématique possible : « toute connaissance rationnelle a lieu ou par concepts ou par construction des concepts ; la première s'appelle philosophique, et la seconde, mathématique ». Construire un concept, c'est l'exhiber dans l'intuition pure : le géomètre ne médite pas sur la définition du triangle, il trace un triangle, sur le papier ou en imagination, et ce triangle singulier vaut pour tous, parce que seul y a été mis ce que le concept exige. Kant illustre la différence par une expérience de pensée restée classique : donnez au philosophe le concept de triangle et demandez-lui ce que valent ses angles ; il pourra l'analyser aussi longtemps qu'il voudra, il n'en tirera rien de neuf. Le géomètre, lui, construit la figure, prolonge un côté, mène une parallèle, et lit sur sa construction que la somme des angles égale deux droits. La démonstration mathématique doit sa fécondité et son évidence à ce recours à l'intuition : elle est, dit Kant, une preuve apodictique conduite dans l'intuition, et c'est à elle seule que convient le nom de démonstration ; les preuves philosophiques, conduites par simples concepts au moyen de mots, sont discursives (Kant dit « acroamatiques ») et n'atteignent jamais cette évidence construite.

Il suit de là que la philosophie ne doit imiter ni les définitions, ni les axiomes, ni les démonstrations des mathématiques. Ses concepts lui sont donnés, confus, à clarifier, non construits à volonté ; ses principes ne sont pas évidents par intuition ; ses preuves doivent avancer sans le secours d'aucune figure. Le more geometrico de Spinoza et de l'école wolffienne repose donc, aux yeux de Kant, sur une méprise quant à la source de la certitude mathématique : on peut emprunter à Euclide sa mise en page, non son intuition. Kant ne condamne pas pour autant la philosophie à l'à-peu-près ; il lui assigne d'autres types de preuves, dont sa propre Critique offre les modèles. La « déduction transcendantale » des catégories n'est pas une dérivation au sens des géomètres : le mot est emprunté aux juristes, chez qui la déduction établit la légitimité d'une possession (quid juris) et non un fait ; elle démontre, si l'on veut, mais en montrant que sans les catégories aucune expérience ne serait possible. Quant aux preuves prétendues de l'existence de Dieu, l'argument ontologique en tête, Kant les défait en montrant qu'on ne tire pas l'existence d'un concept : l'être n'est pas un prédicat réel qui s'ajouterait à la notion d'une chose, et cent thalers pensés contiennent exactement ce que contiennent cent thalers réels. Leçon durable : chaque domaine du savoir a le type de preuve que son objet permet, et le premier devoir d'une épistémologie est de ne pas exiger d'un champ les démonstrations d'un autre. Restait une hypothèse que Kant ne discutait guère, tant elle semblait sûre : que la géométrie d'Euclide décrit l'espace, le seul espace possible, et que ses axiomes sont des jugements synthétiques a priori à la fois nécessaires et évidents. C'est elle que le XIX^e siècle allait ruiner.

La crise des évidences

La chute du postulat des parallèles

Le cinquième postulat d'Euclide affirme, sous sa forme moderne, que par un point extérieur à une droite passe une parallèle à cette droite et une seule. Dès l'Antiquité, son manque d'évidence a paru une tache sur le monument : Proclus déjà voulait le démontrer. Deux mille ans d'efforts ont suivi, dont l'épisode le plus instructif est le livre du jésuite Girolamo Saccheri, Euclides ab omni naevo vindicatus (1733), « Euclide lavé de toute tache » : pour prouver le postulat, Saccheri en suppose la négation et développe les conséquences, espérant buter sur une contradiction. La contradiction ne vient pas ; elle ne viendra jamais, et Saccheri, sans le savoir, démontrait les premiers théorèmes d'une autre géométrie. Au début du XIX^e siècle, Gauss en privé, puis Lobatchevski (1829) et Bolyai (1832) publiquement, franchissent le pas : ils construisent une géométrie complète où, par un point, passent une infinité de parallèles à une droite donnée, et où la somme des angles d'un triangle est inférieure à deux droits. Riemann généralise en 1854, et propose au passage une géométrie sans aucune parallèle. Restait un doute : ces géométries étranges ne cachaient-elles pas une contradiction encore inaperçue ? La réponse vint par une invention qui allait transformer l'idée de preuve : le modèle. Beltrami (1868), puis Klein et Poincaré, montrent qu'on peut interpréter tous les termes de la géométrie de Lobatchevski dans des objets euclidiens (les « droites » devenant, par exemple, des cordes d'un cercle ou des demi-cercles orthogonaux à une droite fixe) de sorte que tous ses axiomes deviennent des théorèmes euclidiens. Conséquence : si la géométrie d'Euclide est cohérente, celle de Lobatchevski l'est aussi. Toute contradiction chez la seconde se traduirait en contradiction chez la première.

Il faut mesurer ce que cet épisode change au concept de démonstration. D'abord, un type de résultat inédit apparaît : la preuve d'indémontrabilité. Montrer que le postulat des parallèles ne se déduit pas des autres axiomes, c'est démontrer qu'aucune démonstration n'existe, ce que nul échec particulier, fût-il répété deux mille ans, ne pouvait établir ; l'instrument en est le modèle, qui réalise les axiomes en falsifiant l'énoncé visé. Ensuite, les axiomes perdent leur statut d'évidences : deux géométries incompatibles ne peuvent être toutes deux des descriptions nécessaires de l'espace. Poincaré tirera la conclusion dans une page fameuse : « Les axiomes géométriques ne sont donc ni des jugements synthétiques à priori ni des faits expérimentaux. Ce sont des conventions » ; notre choix parmi les conventions possibles est guidé par l'expérience, mais reste libre, et demander si la géométrie euclidienne est vraie n'a pas plus de sens que demander si le mètre est vrai. Qu'on suive ou non ce conventionnalisme, une chose est acquise : la démonstration ne transmet plus la vérité depuis des sources évidentes ; elle établit des liens conditionnels. Si les axiomes, alors le théorème. Russell donnera de ce tournant hypothético-déductif la formule la plus abrupte, en ouverture de ses Principles of Mathematics : les mathématiques pures sont la classe de toutes les propositions de la forme « p implique q ».

La même époque découvre que l'évidence n'est pas seulement dispensable : elle est trompeuse. L'analyse du XVIII^e siècle maniait ses infiniment petits avec un bonheur que la rigueur ne suivait pas ; le XIX^e siècle paie la dette. Cauchy, puis Weierstrass, reconstruisent limites, continuité et dérivées sur des définitions en epsilon et delta qui ne doivent plus rien à l'intuition du mouvement ; et cette rigueur nouvelle exhibe des monstres qui donnent tort à la vision : en 1872, Weierstrass construit une fonction continue en tout point et dérivable en aucun, une courbe sans tangente nulle part, que nulle imagination ne peut se figurer. La leçon est double. L'intuition, guide vénéré depuis les Grecs, peut égarer ; et des êtres mathématiques parfaitement définis échappent à toute représentation. La démonstration change alors de fonction : elle n'est plus le chemin balisé qui mène une évidence vers une autre, elle devient l'unique organe d'accès à des objets que l'œil intérieur ne voit plus. Gaston Bachelard élèvera ce constat en principe pour toute la connaissance scientifique : « Rien ne va de soi. Rien n'est donné. Tout est construit » ; l'évidence première y figure parmi les obstacles que la preuve a pour tâche de rectifier, non parmi les fondements sur lesquels elle s'appuierait.

Frege : la preuve sans lacune

Page de titre de la Begriffsschrift (1879) de Gottlob Frege, « idéographie » conçue pour que les démonstrations s'écrivent sans aucune lacune.

Si l'intuition peut tricher, il faut lui interdire l'entrée des démonstrations. Tel est le projet que Gottlob Frege, mathématicien à Iéna, expose en 1879 dans un opuscule au titre austère, Begriffsschrift, « écriture conceptuelle » ou idéographie : une langue de formules pour la pensée pure, où chaque inférence s'accomplit selon des règles explicites, de sorte que la chaîne déductive soit sans lacune (lückenlos) et qu'aucun présupposé intuitif ne puisse s'y glisser inaperçu. L'outil déborde de loin la vieille syllogistique : Frege y invente la quantification, l'analyse des énoncés en fonction et argument, bref la logique moderne, la plus grande refonte de la discipline depuis Aristote. L'enjeu n'est pas seulement technique. Frege veut trancher une question philosophique : l'arithmétique doit-elle quelque chose à l'intuition, comme le soutenait Kant pour qui 7 + 5 = 12 est synthétique a priori, ou est-elle réductible à la pure logique ? Sa réponse, le logicisme, se joue entièrement sur le terrain de la démonstration : une vérité sera dite analytique si sa preuve ne mobilise que des lois logiques générales et des définitions, synthétique a priori si elle requiert en outre des principes d'une science particulière. La nature d'une proposition ne se lit plus dans son contenu, mais dans l'arbre généalogique de sa démonstration : il fallait donc des démonstrations intégrales, où chaque emprunt fût visible. Les Fondements de l'arithmétique (1884) définissent le nombre en termes logiques ; les Lois fondamentales de l'arithmétique (1893-1903) entreprennent la dérivation formelle complète.

On sait la suite, l'une des scènes les plus dramatiques de l'histoire des sciences. En juin 1902, alors que le second volume des Lois fondamentales est sous presse, Frege reçoit une lettre d'un jeune logicien anglais, Bertrand Russell, qui lui signale une difficulté : sa loi V permet de former l'ensemble des ensembles qui ne s'appartiennent pas à eux-mêmes ; or cet ensemble s'appartient si et seulement s'il ne s'appartient pas. La contradiction loge au cœur du système. Frege publie la lettre en appendice, avec une loyauté restée exemplaire, notant qu'il n'est guère de sort plus fâcheux pour un auteur scientifique que de voir l'un des fondements de son édifice ébranlé quand l'ouvrage s'achève. La leçon vaut d'être méditée : la formalisation intégrale, conçue pour rendre l'erreur impossible, n'immunise pas contre la contradiction, car elle ne dispense pas de choisir des axiomes, et l'axiome le plus limpide en apparence (quel énoncé semblait plus innocent que : à tout concept correspond l'ensemble des objets qui tombent sous lui ?) peut receler l'incohérence. Russell lui-même, avec Whitehead, tentera de sauver le programme logiciste dans les Principia Mathematica (1910-1913), au prix d'une théorie des types qui hiérarchise les ensembles et d'un appareil formel d'une ampleur inouïe : la proposition établissant, en substance, que 1 + 1 = 2 n'y est complètement démontrée qu'au deuxième volume, les auteurs notant avec un flegme resté célèbre que l'énoncé est « à l'occasion utile ».

Hilbert : la démonstration devient un objet

David Hilbert en 1912. Sa « théorie de la démonstration » fait des preuves elles-mêmes des objets d'étude mathématique.

C'est à David Hilbert que revient le pas suivant, le plus gros de conséquences pour notre notion. Ses Fondements de la géométrie (1899) réécrivent Euclide selon une exigence nouvelle : les termes primitifs (point, droite, plan) n'y sont plus définis par des évidences, mais implicitement, par les seules relations que les axiomes leur imposent ; et la validité d'une démonstration ne doit dépendre que de ces relations, jamais du sens ou de l'image des termes. Hilbert en donnait une formule provocante, rapportée par son biographe : on doit pouvoir dire à tout moment, au lieu de « points, droites, plans », « tables, chaises, chopes de bière », sans qu'aucune démonstration cesse de valoir. La boutade enterre deux mille ans de conception intuitive : une démonstration n'est plus une suite d'évidences vues, c'est une structure dont la correction se contrôle indépendamment de toute interprétation. Restait à exploiter cette découverte. Puisqu'une preuve formalisée n'est qu'un assemblage fini de signes obéissant à des règles explicites, elle est elle-même un objet mathématique, au même titre qu'un nombre ou un polyèdre ; on peut donc faire des mathématiques sur les démonstrations, démontrer des théorèmes à leur sujet. Hilbert baptise cette discipline nouvelle métamathématique ou théorie de la démonstration (Beweistheorie), et lui assigne dans les années 1920 une mission précise, connue sous le nom de programme de Hilbert : formaliser les mathématiques, puis démontrer, par des moyens élémentaires et incontestables (finitistes, dit-il), que ces systèmes formels sont cohérents, c'est-à-dire qu'on n'y démontrera jamais une contradiction.

Le programme répond à une crise. Les paradoxes de la théorie des ensembles ont ébranlé la confiance ; et une école dissidente, menée par Brouwer, propose d'y couper court en amputant les mathématiques de leurs raisonnements non constructifs. Hilbert refuse la mutilation : « Personne ne doit pouvoir nous chasser du paradis que Cantor a créé pour nous » ; et retirer au mathématicien le tiers exclu, ce serait, écrit-il, comme interdire au boxeur l'usage de ses poings. Mais ce refus se veut payé comptant : la sécurité perdue de l'évidence sera remplacée par une démonstration de non-contradiction. Le pari est immense, et l'optimisme de Hilbert sans réserve ; il le proclame en 1930 à Königsberg, dans une allocution dont la péroraison sera gravée sur sa tombe : nous devons savoir, nous saurons. L'ironie de l'histoire a voulu que, la veille de ce discours, dans la même ville, un jeune logicien de Vienne annonce discrètement un résultat qui allait ruiner le programme dans sa forme initiale. Il s'appelait Kurt Gödel.

Brouwer : démontrer, c'est construire

Avant d'en venir à Gödel, il faut présenter l'adversaire que Hilbert affrontait, car la dispute porte sur le sens même du mot démontrer. Pour le mathématicien néerlandais L. E. J. Brouwer, fondateur de l'intuitionnisme, les mathématiques ne sont pas un langage ni un système formel : elles sont une activité de construction mentale, et un énoncé mathématique n'est vrai que si nous avons effectué la construction qu'il affirme. Démontrer qu'un objet existe, c'est le construire, ou donner un procédé qui le construit ; démontrer une disjonction, c'est démontrer l'un des deux membres. De là un rejet qui fit scandale : le principe du tiers exclu, « A ou non-A », cesse d'être une loi fiable dès qu'on quitte les totalités finies. Affirmer « A ou non-A » à propos, disons, d'une propriété portant sur tous les entiers, c'est prétendre qu'on possède soit une preuve de A, soit une preuve de non-A ; or, pour la plupart des conjectures ouvertes (celle de Goldbach, par exemple : tout nombre pair supérieur à 2 est somme de deux nombres premiers), nous n'avons ni l'une ni l'autre. Le classique dira : l'énoncé est pourtant vrai ou faux en soi. L'intuitionniste répond : ce « en soi » est un acte de foi métaphysique ; en mathématiques, la vérité ne devance pas la preuve.

Un exemple standard fait toucher du doigt l'enjeu, et il est si instructif que les manuels de logique le reprennent. Démontrons qu'il existe deux nombres irrationnels a et b tels que a puissance b soit rationnel. Considérons r, égal à racine de 2 élevée à la puissance racine de 2. Ou bien r est rationnel, et l'on prend a et b égaux à racine de 2 ; ou bien r est irrationnel, et l'on prend a égal à r et b égal à racine de 2, car alors a puissance b vaut racine de 2 élevée à la puissance 2, c'est-à-dire 2. Dans les deux cas, l'existence est établie : la démonstration est classiquement irréprochable. Mais elle ne nous dit pas lequel des deux couples convient ; elle prouve qu'un objet existe sans en exhiber aucun. Pour l'intuitionniste, une telle preuve n'établit pas l'existence au sens fort : elle montre seulement qu'il serait contradictoire qu'aucun couple ne convienne. La logique intuitionniste, dégagée par Heyting, consigne ces exigences : on y renonce au tiers exclu et au raisonnement par l'absurde comme preuve d'existence, et l'on y explique le sens des connecteurs par les preuves plutôt que par les conditions de vérité : une preuve de « A et B » est un couple de preuves, une preuve de « A implique B » est un procédé transformant toute preuve de A en preuve de B, une preuve de « il existe x tel que A » est un témoin accompagné d'une preuve. Idée neuve entre toutes : la démonstration cesse d'être un moyen d'accéder à la vérité pour devenir ce qui constitue le sens des énoncés. On la retrouvera, sous d'autres habits, dans l'informatique contemporaine.

Gödel : la vérité déborde la preuve

Kurt Gödel a démontré coup sur coup les deux théorèmes qui bornent, l'un par le haut, l'autre par le bas, les pouvoirs de la démonstration formelle. Le premier, sa thèse de 1929 publiée en 1930, est un succès complet pour le point de vue formel : c'est le théorème de complétude de la logique du premier ordre. Les quelques règles de déduction dégagées depuis Frege suffisent exactement à leur tâche : une formule est démontrable à partir d'axiomes si et seulement si elle est vraie dans toute interprétation qui rend ces axiomes vrais. Rien de ce qui est logiquement valide n'échappe donc au filet des règles : il n'était pas évident qu'un nombre fini de règles pût suffire à démontrer tout ce qui est vrai en ce sens, et c'est ce que ce théorème, dont la preuve n'a rien de trivial, garantit. La conséquence philosophique mérite d'être soulignée : au niveau de la pure logique, vérité (dans toutes les interprétations) et démontrabilité coïncident. Tout l'aplomb du formalisme tient dans cette coïncidence.

Encore fallait-il que chacun des deux membres de l'équivalence eût un sens exact. Le membre syntaxique, être démontrable, l'avait reçu de Frege et de Hilbert : exister au sommet d'un arbre de règles. Le membre sémantique, être vrai dans toute interprétation, restait une notion intuitive ; c'est Alfred Tarski qui lui donne sa forme mathématique, en définissant d'abord ce que signifie « vrai dans une structure » (1933), puis la conséquence logique (1936) : une formule est conséquence de prémisses quand toute interprétation qui rend vraies les prémisses la rend vraie aussi. Le théorème de complétude prend alors son énoncé définitif : la relation syntaxique de démontrabilité et la relation sémantique de conséquence, définies par des voies entièrement différentes, l'une par des règles, l'autre par des interprétations, ont exactement la même étendue. Deux notions, une seule extension : c'est la distinction annoncée plus haut, au sortir d'Aristote, qui trouve ici et sa formulation rigoureuse et son théorème.

Elle se brise un étage plus haut. En 1931, Gödel publie l'article le plus commenté de la logique moderne, « Sur des propositions formellement indécidables des Principia Mathematica et des systèmes apparentés ». Son premier théorème d'incomplétude établit ceci : toute théorie cohérente, donnée par un ensemble d'axiomes reconnaissable par un procédé effectif, et assez riche pour contenir l'arithmétique élémentaire, est incomplète ; il existe des énoncés arithmétiques qu'elle ne démontre pas et dont elle ne démontre pas non plus la négation. L'ingéniosité de la preuve est restée légendaire : Gödel code les formules et les démonstrations par des nombres entiers, si bien que « être démontrable » devient une propriété arithmétique ; il construit alors, par un argument diagonal, un énoncé G qui affirme, à travers ce codage, sa propre indémontrabilité. La parenté avec le paradoxe du menteur saute aux yeux, à une différence près qui change tout : G ne dit pas « je suis faux », ce qui engendrerait une contradiction, mais « je ne suis pas prouvable ». Si la théorie est cohérente, elle ne démontre pas G ; mais alors ce que G affirme est le cas, et G est vrai dans les entiers standard sans y être démontrable. Le second théorème enfonce le clou au point précis où Hilbert espérait bâtir : une telle théorie, si elle est cohérente, ne peut pas démontrer l'énoncé arithmétique qui exprime sa propre cohérence. La cohérence de l'arithmétique ne se prouvera pas avec les seuls moyens de l'arithmétique, ni, à plus forte raison, avec les moyens plus faibles que le programme finitiste s'autorisait.

Que retenir, philosophiquement, de ce coup de tonnerre ? D'abord une dissociation : vérité et démontrabilité, que Leibniz rêvait de confondre et que la complétude identifiait au niveau logique, se séparent au niveau des théories mathématiques. Aucun système formel cohérent n'épuise les vérités de l'arithmétique ; la démontrabilité est toujours relative à un système, que l'on peut certes renforcer (en ajoutant G comme axiome, par exemple), mais le système renforcé engendre son propre énoncé indécidable, et ainsi sans terme. Ensuite, une réhabilitation paradoxale : c'est par une démonstration, et par l'une des plus rigoureuses jamais écrites, que les limites de la démonstration ont été fixées ; le théorème de Gödel n'est pas une défaite de la raison démonstrative, mais l'un de ses triomphes, la preuve prenant pour objet ses propres frontières. Enfin, une invitation à la prudence : le théorème porte sur les systèmes formels satisfaisant des hypothèses précises, non sur « la raison » ou « l'esprit humain » en général, et les usages qui lui font dire que toute pensée est incomplète ou que la science ne peut se fonder outrepassent ce qu'il énonce ; savoir qu'un théorème parfaitement démontrable dans la théorie des ensembles échappe aux seuls axiomes de Peano laisse d'ailleurs les mathématiciens sereins, eux qui n'ont jamais fixé par avance la liste de leurs méthodes. Le programme de Hilbert lui-même n'est pas mort de sa mort brutale : en 1936, Gerhard Gentzen démontre la cohérence de l'arithmétique de Peano, au prix d'un principe (une récurrence transfinie le long d'un bon ordre noté epsilon zéro) qui excède ce que l'arithmétique formalise ; la théorie de la démonstration y a gagné son style propre, mesurer la force des théories à l'aune des principes nécessaires pour prouver leur cohérence.

La théorie de la démonstration

De Gentzen aux assistants de preuve, un même mouvement se déploie, et il vaut la peine d'en retenir d'avance le fil, car les sections qui suivent sont les plus techniques de cet article. Quatre temps : la démonstration devient un objet doté d'une forme propre ; cet objet révèle sa structure et ses théorèmes ; cette structure se révèle être celle d'un calcul, d'un programme ; et ce programme, une machine peut l'exécuter ou le vérifier. Qui garde ce fil en main ne se perdra pas dans les détails.

La déduction naturelle

Premier temps : donner à l'objet une forme fidèle au raisonnement qu'il capture. Une fois admis que les démonstrations sont des objets, encore faut-il des formalismes qui leur ressemblent. Les systèmes hérités de Frege et de Hilbert, faits de nombreux axiomes et de très peu de règles, produisent des dérivations correctes mais méconnaissables, où le mathématicien ne retrouve pas ses gestes. En 1934, Gerhard Gentzen, élève de l'école de Göttingen, se donne pour but un formalisme aussi proche que possible du raisonnement réel : ce sera la déduction naturelle. Son principe est simple et parlant : à chaque connecteur logique sont associées des règles d'introduction, qui disent comment on démontre un énoncé de cette forme, et des règles d'élimination, qui disent ce qu'on peut en tirer. Pour démontrer « A et B », démontrer A et démontrer B ; de « A et B », tirer A, ou tirer B. Pour démontrer « A implique B », supposer A et démontrer B sous cette hypothèse, qu'on décharge ensuite ; de « A implique B » et de A, tirer B (l'antique modus ponens). Le raisonnement sous hypothèse, geste quotidien du mathématicien (« supposons F et montrons G »), reçoit ainsi droit de cité dans le formalisme : une démonstration y est un assemblage de séquents, c'est-à-dire de couples formés d'un ensemble d'hypothèses et d'une conclusion, et cet assemblage a la forme d'un arbre fini dont chaque nœud est justifié par une règle.

Deux traits de ce dispositif nourrissent la réflexion philosophique. Le premier est son économie : une douzaine de règles, les mêmes pour toutes les mathématiques ; ce qui distingue l'arithmétique de la géométrie ou de l'analyse, ce ne sont pas des logiques différentes, ce sont des axiomes différents, traités comme des hypothèses permanentes. Tout ce qu'il y a de général dans l'acte de raisonner tient donc en une page ; le lecteur qu'étonne cette brièveté mesurera par contraste l'immensité de ce que les axiomes, eux, doivent porter. Le second trait est plus discret : les règles d'introduction ressemblent fort à une définition des connecteurs par leur usage. Savoir ce que signifie « et », n'est-ce pas exactement savoir ce qui compte comme preuve d'une conjonction, et ce qu'on est en droit d'en tirer ? Des logiciens et des philosophes, Dag Prawitz et Michael Dummett en tête, ont élaboré cette intuition en une sémantique des preuves, où le sens d'un énoncé est donné par ses conditions de démontrabilité plutôt que par ses conditions de vérité ; l'harmonie requise entre règles d'introduction et d'élimination y sert de garde-fou, et l'ensemble fournit à l'antiréalisme contemporain son arsenal technique. Qu'on adhère ou non à cette philosophie, un renversement s'y accomplit : la démonstration n'est plus seulement le véhicule du sens, elle en devient la source.

L'élimination des coupures

Deuxième temps : l'objet une fois construit, on peut démontrer des théorèmes à son sujet. Le chef-d'œuvre de Gentzen est justement un théorème sur les démonstrations elles-mêmes. Dans le calcul des séquents, variante symétrique de la déduction naturelle qu'il introduit dans le même mémoire, une règle occupe une place à part : la coupure, qui autorise à utiliser un résultat intermédiaire, un lemme, démontré à part puis « coupé » dans la suite du raisonnement. C'est le geste le plus commun de la pratique mathématique : on ne redémontre pas Pythagore chaque fois qu'on s'en sert. Le théorème fondateur de Gentzen, son Hauptsatz, établit que cette règle est éliminable : toute démonstration peut être transformée, par un procédé effectif, en une démonstration de la même conclusion qui n'emploie aucune coupure. Une démonstration sans coupure a une propriété précieuse, dite de la sous-formule : elle ne fait intervenir que des morceaux de sa conclusion et de ses hypothèses ; rien d'étranger, aucun détour, aucune idée venue d'ailleurs. On en tire presque sans effort la cohérence du calcul : une contradiction, si elle était démontrable, le serait sans coupure, donc par une preuve ne contenant que des sous-formules de l'absurde ; or nulle règle ne permet de conclure ainsi.

La portée philosophique du résultat est double. D'un côté, il réalise localement le rêve d'une preuve entièrement analytique, qui ne sort jamais de son sujet : les coupures éliminées, la démonstration devient une pure explicitation de l'énoncé. De l'autre, il révèle le prix de cette pureté : l'élimination des coupures fait exploser la taille des preuves, parfois au-delà de toute mesure raisonnable. Les lemmes, les détours, les concepts auxiliaires ne sont donc pas des commodités contingentes ; ils sont ce qui rend les démonstrations humainement possibles, l'économie cognitive sans laquelle la déduction resterait un droit sans usage. La structure fine des démonstrations, leurs symétries, la dynamique de leur normalisation sont devenues depuis Gentzen un continent mathématique à part entière, exploré en France notamment par Jean-Yves Girard ; la démonstration y est étudiée comme d'autres étudient les groupes ou les surfaces, avec ses invariants et ses théorèmes de structure.

Des preuves aux programmes

Troisième temps, le plus inattendu : l'objet se met à calculer. La théorie de la démonstration réservait là une surprise que nul programme de recherche n'avait prévue. Dans les années 1930 à 1960, Haskell Curry, puis William Howard, constatent une coïncidence troublante : les règles de la déduction naturelle intuitionniste sont, trait pour trait, les règles de typage du lambda-calcul, le formalisme des fonctions calculables inventé par Alonzo Church. La correspondance, dite de Curry-Howard, se laisse énoncer en trois équations : les propositions sont des types de données ; les démonstrations sont des programmes ; la normalisation des démonstrations (l'élimination de leurs détours) est l'exécution des programmes. Une preuve intuitionniste de « A implique B » n'est pas seulement analogue à une fonction : c'en est une, qui transforme toute donnée de type A en donnée de type B. L'interprétation de Brouwer, Heyting et Kolmogorov, qui expliquait le sens des connecteurs par les preuves, trouve ici sa réalisation littérale, et la vieille constructivité intuitionniste devient un théorème d'extraction : d'une démonstration intuitionniste qu'un objet existe, un algorithme tire l'objet lui-même.

Il est peu de résultats dont la portée conceptuelle soit aussi grande. Deux notions élaborées indépendamment, dans des traditions étrangères l'une à l'autre, la preuve des logiciens et le programme des informaticiens, se révèlent être une seule et même chose regardée sous deux angles. La démonstration cesse d'être un certificat inerte : elle est un opérateur, quelque chose qui calcule ; et le contenu d'un théorème d'existence se mesure désormais à ce que sa preuve permet effectivement de construire. Sur cette base ont été bâtis les assistants de preuve, logiciels où l'utilisateur développe une démonstration que la machine vérifie pas à pas en la traitant comme un programme à typer : Coq, issu du calcul des constructions de Thierry Coquand et Gérard Huet, Lean, Isabelle, ou PhoX, développé par l'un des auteurs du manuel cité au fil de cet article. La boucle leibnizienne se referme étrangement : démontrer est bien devenu calculer, mais non parce que la pensée s'est réduite au calcul ; parce que la notion de calcul s'est élevée jusqu'à héberger la structure des preuves.

L'ordinateur démonstrateur

Dernier temps : puisqu'une démonstration est un objet fini, et même un programme, la machine peut s'en saisir. L'ordinateur est entré dans la démonstration par deux portes, qu'il importe de distinguer. La première est la recherche automatique de preuves. Dès lors que démontrer se ramène à construire un objet fini selon des règles, une machine peut chercher : on peut même, en principe, énumérer toutes les démonstrations possibles et guetter celle qui conclut à la formule voulue ; si elle est démontrable, on la trouvera, fût-ce en quelques milliards d'années, mais si elle ne l'est pas, l'énumération ne s'arrêtera jamais, et l'on n'en saura rien. Les méthodes sérieuses (unification, tableaux, résolution) font mieux que cette énumération aveugle et remportent des succès réels sur des classes de problèmes délimitées ; mais l'essentiel de la démonstration mathématique vivante reste hors de leur portée, et les théorèmes de limitation garantissent qu'aucun perfectionnement n'y changera rien en général.

La seconde porte a fait entrer la machine au cœur d'un débat philosophique. En 1976, Kenneth Appel et Wolfgang Haken annoncent la démonstration du théorème des quatre couleurs : toute carte plane peut être coloriée avec quatre couleurs sans que deux régions voisines partagent la même. Leur preuve réduit le problème à l'examen de près de deux mille configurations, examen confié à un ordinateur au terme de plus d'un millier d'heures de calcul. Aucun être humain n'a vérifié à la main, ni ne vérifiera jamais, l'ensemble de ces configurations : la partie machinale de la preuve excède ce qu'une vie de lecteur peut parcourir. Est-ce encore une démonstration ? Le philosophe Thomas Tymoczko soutint que non, ou du moins que le savoir ainsi obtenu changeait de nature, cessant d'être a priori pour devenir tributaire, comme une expérience de physique, de la fiabilité d'un appareil. L'objection retrouve une exigence ancienne, que Wittgenstein avait placée au centre de ses remarques sur les mathématiques : une démonstration doit pouvoir être embrassée du regard (übersehbar), reproduite, prise comme modèle ; ce qui ne peut être survolé ainsi change de statut.

L'histoire ultérieure a déplacé le débat plus qu'elle ne l'a clos. En 1998, Thomas Hales annonce une démonstration de la conjecture de Kepler sur l'empilement optimal des sphères, par une stratégie du même type ; la revue qui la publie en 2005, après plusieurs années d'expertise, fait savoir que ses rapporteurs, tout en étant convaincus, n'ont pu certifier entièrement la partie calculatoire. Réponse de Hales : faire vérifier la preuve entière, calculs compris, par un assistant de preuve, dont le noyau logique, minuscule, peut être inspecté ligne à ligne ; le projet, baptisé Flyspeck, aboutit en 2014, et la preuve formelle paraît en 2017. Georges Gonthier avait fait de même pour les quatre couleurs en 2005, puis, avec son équipe, pour le théorème de Feit et Thompson en théorie des groupes. Le déplacement est instructif : la confiance ne va plus à la lecture humaine d'un texte, mais à la vérification mécanique d'un objet formel, la part de foi se concentrant sur un vérificateur assez petit pour être, lui, entièrement lu. Nul ne « voit » davantage pourquoi quatre couleurs suffisent ; mais la certitude que la preuve est correcte a été portée à un degré que les démonstrations classiques, avec leurs coquilles et leurs sous-entendus, n'atteignent pas toujours. La question de Descartes, comment garantir une chaîne trop longue pour un seul regard, a reçu une réponse que Descartes n'aurait pas devinée : on ne demande plus à Dieu de garantir la mémoire du géomètre, on demande au géomètre de vérifier le vérificateur.

Questions ouvertes

Ce que la Tortue dit à Achille

En 1895, Lewis Carroll, logicien de son état sous le nom de Charles Dodgson, publie dans la revue Mind un dialogue de trois pages qui n'a pas fini d'occuper les philosophes. La Tortue soumet à Achille un raisonnement en deux prémisses, A et B, dont Z suit logiquement ; elle accorde A, elle accorde B, mais se refuse à accorder Z, tant qu'on ne lui aura pas accordé aussi la proposition C : « si A et B sont vraies, Z doit être vraie ». Achille, bonne pâte, inscrit C sur son carnet. La Tortue accorde C, mais demande alors D : « si A, B et C sont vraies, Z doit être vraie ». Et ainsi de suite ; au bout de quelques mois, le carnet compte plusieurs milliers de prémisses, et Z n'est toujours pas conclue. La morale de l'apologue, sur laquelle on s'accorde à défaut de s'accorder sur sa formulation exacte, est que les règles d'inférence ne sont pas des prémisses : le passage des prémisses à la conclusion ne peut pas être lui-même une prémisse supplémentaire, sous peine de régression sans fin. Une démonstration ne contient pas la totalité de ce qui la fait fonctionner ; il y faut, en deçà de tout énoncé, une pratique de l'inférence, quelque chose que l'on fait et que l'on ne peut indéfiniment coucher sur le papier. La démonstration la plus complète suppose des démonstrateurs déjà formés, et l'idéal de la preuve intégrale, qui expliciterait jusqu'à ses propres règles d'emploi, rejoint le rêve impossible que Pascal congédiait.

Lakatos : preuves et réfutations

Le philosophe hongrois Imre Lakatos a contesté, documents à l'appui, l'image même que cet article a suivie jusqu'ici : celle d'une démonstration qui, une fois trouvée, établit sa conclusion une fois pour toutes. Preuves et réfutations (1963-1964) reconstitue, sous la forme d'un dialogue de classe, l'histoire réelle d'un théorème d'Euler : pour tout polyèdre, le nombre des sommets moins le nombre des arêtes plus le nombre des faces égale 2. Cauchy en donne une démonstration en 1811. Puis les contre-exemples pleuvent, pendant un demi-siècle : un cube creusé d'une cavité cubique, un polyèdre en forme de cadre de tableau, les polyèdres étoilés de Kepler ; pour chacun, la formule échoue, sans que personne ne trouve d'erreur dans la preuve. Que fait alors la communauté ? Elle ne jette pas la démonstration : elle négocie. Les uns excluent les monstres (« ceci n'est pas un vrai polyèdre »), les autres raffinent le théorème (« pour tout polyèdre convexe... », « pour tout polyèdre simplement connexe... »), et le concept de polyèdre, qui semblait aller de soi, se trouve redéfini par les besoins de la preuve. Lakatos en tire une thèse sur la croissance du savoir mathématique : les démonstrations informelles ne sont pas des dérivations closes, mais des expériences de pensée qui décomposent la conjecture en sous-conjectures ; les réfutations ne les tuent pas, elles les améliorent ; et les concepts mathématiques sont engendrés par ce va-et-vient, la preuve façonnant la définition autant que l'inverse. L'axiomatisation n'arrive qu'ensuite, quand la poussière est retombée. La leçon ne contredit pas la logique ; elle rappelle que la logique décrit des démonstrations achevées, quand la mathématique vivante se fait dans l'atelier, au milieu des copeaux.

Démontrer et argumenter

Que devient, hors des mathématiques, l'exigence démonstrative ? Le droit, la politique, la morale, la critique raisonnent, et pourtant on n'y démontre pas au sens des géomètres : les conclusions y restent discutées entre gens compétents et de bonne foi, ce qui ne se voit guère pour le théorème de Pythagore. Chaïm Perelman, philosophe du droit bruxellois, a construit sur ce constat une réhabilitation de la rhétorique. Le Traité de l'argumentation (1958), écrit avec Lucie Olbrechts-Tyteca, s'ouvre sur le partage : « Le domaine de l'argumentation est celui du vraisemblable, du plausible, du probable, dans la mesure où ce dernier échappe aux certitudes du calcul ». La démonstration, impersonnelle, vaut indépendamment de tout auditoire : correcte ou non, elle n'a pas à convaincre, seulement à être vérifiée. L'argumentation s'adresse au contraire à des esprits qu'il s'agit de gagner ; elle part non d'axiomes mais de lieux communs admis par l'auditoire, avance par accumulation et convergence plutôt que par enchaînement linéaire, et ses conclusions engagent à des degrés divers, sans jamais contraindre. Stephen Toulmin, la même année, aboutissait en Angleterre à un diagnostic voisin : le modèle géométrique, plaqué sur le raisonnement pratique, en méconnaît la structure propre, faite de données, de garanties et de réserves. Ni l'un ni l'autre ne rabaissent la démonstration ; ils bornent son empire, et défendent la rationalité des domaines où elle n'a pas cours. Pascal, on l'a vu, avait ouvert la voie : là où les principes sont trop fins pour être ordonnés, juger n'est pas déduire.

Reste une inquiétude plus sourde, que la littérature a mieux dite que les traités. L'homme du souterrain de Dostoïevski se heurte au « deux fois deux quatre » comme à un mur : la nécessité démontrée ne lui laisse rien à vouloir, rien à être, et il lui préfère, par bravade, un « deux fois deux cinq » qui aurait au moins le mérite d'être sien. La page rappelle ce que l'enthousiasme démonstratif oublie volontiers : la contrainte de la preuve, précieuse pour connaître, peut être vécue comme une violence par la liberté, et il entre dans la sagesse de ne pas demander à la démonstration de régler ce qui relève de la décision. Démontrer à quelqu'un qu'il doit aimer serait le plus sûr moyen de l'en dégoûter.

La démonstration comme acte social

Les mathématiciens eux-mêmes ont rouvert le dossier, en décrivant ce que les logiciens laissent hors champ : la vie des démonstrations dans la communauté qui les produit. Le logicien Yuri Manin l'a dit sans détour : une démonstration ne devient une démonstration qu'après l'acte social qui consiste à l'accepter comme telle. William Thurston, l'un des géomètres majeurs du XX^e siècle, a raconté de l'intérieur ce que cette acceptation suppose : des textes qui ne livrent qu'une part de ce que leurs auteurs savent, une compréhension qui circule par exposés, conversations et apprentissages, et des preuves dont la fiabilité tient moins au détail des symboles qu'à la robustesse d'un réseau d'idées partagées. Les grandes entreprises collectives donnent à ce constat une échelle inédite : la classification des groupes simples finis, achevée pour l'essentiel en 1983 et complétée en 2004, s'étend sur des dizaines de milliers de pages dues à une centaine d'auteurs, et nul individu n'en a vérifié la totalité ; la confiance y est, par construction, distribuée. Et lorsque le réseau se déchire, la notion même de démonstration entre en crise ouverte : la preuve de la conjecture abc proposée en 2012 par Shinichi Mochizuki, publiée en 2021 dans une revue de son institut, reste tenue pour incomplète par une partie de la communauté depuis les objections de Peter Scholze et Jakob Stix en 2018, et le monde mathématique vit, fait rarissime, avec un théorème dont le statut dépend du continent où l'on se trouve.

Faut-il en conclure que la démonstration se dissout dans la sociologie ? Ce serait confondre deux questions. Que la reconnaissance d'une preuve soit un processus social, faillible, historiquement situé, c'est un fait ; qu'il n'y ait rien à reconnaître, c'en serait un autre, que rien n'établit. L'assistant de preuve et le séminaire, la vérification formelle et la conversation de couloir ne s'opposent pas : ce sont deux régimes de contrôle d'un même objet, et leur histoire récente est celle d'une division du travail, la machine certifiant la correction pendant que la communauté juge l'intérêt, la portée, la beauté. Épistémologiquement, la démonstration apparaît alors pour ce qu'elle est depuis Thalès : non pas un ailleurs de la vie sociale, mais l'institution que les hommes ont inventée pour que certains de leurs accords ne dépendent plus de leur bon vouloir. Bachelard aurait dit : une raison qui s'enseigne, et qui n'existe qu'enseignée.

La philosophie démontre-t-elle ?

Il reste à retourner l'instrument contre l'atelier qui l'a forgé. La philosophie, qui a défini, exalté, borné la démonstration, démontre-t-elle elle-même ? Le spectacle des doctrines qui s'affrontent depuis vingt-cinq siècles suggère que non : aucun théorème philosophique n'a jamais clos une controverse comme la proposition IX, 20 d'Euclide a clos la question du nombre des nombres premiers. Kant en avait donné la raison de principe : privée de la construction des concepts, la philosophie n'a pas de démonstrations, seulement des preuves discursives, exposées à la contestation de leurs prémisses. L'histoire des grandes preuves philosophiques semble lui donner raison : l'argument ontologique, démonstration en bonne et due forme de l'existence de Dieu aux yeux d'Anselme, de Descartes et de Leibniz, est tenu pour un paralogisme par Thomas d'Aquin, par Kant, par la plupart des modernes ; le doute hyperbolique, le pari, l'impératif catégorique ont connu des fortunes semblables. Ce que la philosophie appelle preuve désigne, semble-t-il, ce qu'un adversaire compétent appellera pétition de principe.

Le tableau demande pourtant deux retouches. La première : la philosophie dispose de formes de preuve qui lui sont propres, et qui ne se réduisent pas à la déduction depuis des axiomes contestables. La réfutation par rétorsion, inaugurée par Aristote pour défendre le principe de non-contradiction, établit sa conclusion en montrant que l'adversaire la présuppose dans l'acte même de la nier ; les arguments dits transcendantaux concluent des conditions sans lesquelles une expérience ou une pratique reconnue de tous ne serait pas possible ; l'analyse d'exemples et de cas limites, l'expérience de pensée, la mise en contradiction d'un système avec lui-même sont des opérations réglées, contrôlables, enseignables. Preuves faillibles, preuves discutées ; mais la section précédente a montré que la discussion n'est pas l'autre de la preuve, elle est son milieu de vie. La seconde retouche : l'absence de résultats définitifs n'équivaut pas à l'absence de progrès. Des arguments ont été définitivement écartés, des distinctions définitivement acquises, des positions contraintes de se raffiner sous la pression d'objections démonstratives ; la carte des positions possibles, en philosophie de la connaissance ou de l'esprit, est incomparablement plus fine qu'au temps de Descartes, et c'est à des raisonnements qu'on le doit.

Peut-être faut-il alors renverser la question. Demander si la philosophie démontre, c'est encore mesurer toute preuve à l'étalon géométrique, ce more geometrico dont cet article a raconté la grandeur et les déboires. Or s'il est une chose que l'histoire de la démonstration enseigne, c'est que la démonstration a une histoire : ses normes ont changé, d'Euclide à Weierstrass et de Frege aux assistants de preuve ; ses pouvoirs ont été bornés de l'intérieur, par ses propres théorèmes ; son autorité s'est révélée solidaire d'une pratique, d'une communauté, d'un apprentissage. La philosophie n'a pas à rougir de ne pas démontrer comme la géométrie, car la géométrie elle-même n'a jamais démontré comme la géométrie rêvée. Ce qui demeure, du papyrus d'Oxyrhynque aux écrans de Coq, c'est l'engagement que le mot grec portait déjà : ne rien avancer qu'on ne soit prêt à faire voir, pas à pas, à quiconque prendra la peine de suivre. La démonstration n'est pas le tout de la raison ; elle en est la promesse tenue le plus longtemps.

Bibliographie

Sources

• Aristote (trad. Jules Tricot), Seconds Analytiques, Paris, Vrin, 1938
• Euclide (trad. Bernard Vitrac), Les Éléments, Paris, Presses universitaires de France, 1990-2001 (4 volumes).
• René Descartes, Œuvres philosophiques, Paris, Garnier, 1963-1973 (3 volumes, éd. Ferdinand Alquié).
• Blaise Pascal, Œuvres complètes, Paris, Seuil, 1963 (éd. Louis Lafuma ; contient De l'esprit géométrique et les Pensées).
• Averroès (trad. Marc Geoffroy), Discours décisif, Paris, GF-Flammarion, 1996
• Thomas d'Aquin, Somme théologique, Paris, Cerf, 1984-1986 (4 volumes).
• Baruch Spinoza (trad. Charles Appuhn), Éthique, Paris, Garnier-Flammarion, 1965
• Gottfried Wilhelm Leibniz, La Monadologie, Paris, Delagrave, 1881 (éd. Émile Boutroux).
• Emmanuel Kant (trad. Alexandre J.-L. Delamarre et François Marty), Critique de la raison pure, Paris, Gallimard, 1980
• Gottlob Frege (trad. Claude Imbert), Les Fondements de l'arithmétique, Paris, Seuil, 1969
• Gottlob Frege (trad. Corine Besson), Idéographie, Paris, Vrin, 1999
• Henri Poincaré, La Science et l'Hypothèse, Paris, Flammarion, 1902
• Henri Poincaré, Science et méthode, Paris, Flammarion, 1908
• Jean Largeault (éd.), Intuitionnisme et théorie de la démonstration, Paris, Vrin, 1992
• Alfred Tarski, Logique, sémantique, métamathématique, Paris, Armand Colin, 1972-1974 (2 volumes).
• Ludwig Wittgenstein (trad. Marie-Anne Lescourret), Remarques sur les fondements des mathématiques, Paris, Gallimard, 1983

Études

• Gaston Bachelard, La Formation de l'esprit scientifique, Paris, Vrin, 1938
• Robert Blanché, L'Axiomatique, Paris, Presses universitaires de France, 1955
• Jean Cavaillès, Méthode axiomatique et formalisme, Paris, Hermann, 1938
• René David, Karim Nour et Christophe Raffalli, Introduction à la logique. Théorie de la démonstration, Paris, Dunod, 2003 (2^e édition).
• Gilles Dowek, Les Métamorphoses du calcul. Une étonnante histoire de mathématiques, Paris, Le Pommier, 2007
• Jean-Yves Girard, Le Point aveugle. Cours de logique, Paris, Hermann, 2006-2007 (2 volumes).
• Imre Lakatos (trad. Nicolas Balacheff et Jean-Marie Laborde), Preuves et réfutations. Essai sur la logique de la découverte mathématique, Paris, Hermann, 1984
• Geoffrey E. R. Lloyd (trad. Jeanne Carlier), Origines et développement de la science grecque. Magie, raison et expérience, Paris, Flammarion, 1990
• Alain de Libera, La Philosophie médiévale, Paris, Presses universitaires de France, 1993
• Ernest Nagel, James R. Newman, Kurt Gödel et Jean-Yves Girard, Le Théorème de Gödel, Paris, Seuil, 1989
• Chaïm Perelman et Lucie Olbrechts-Tyteca, Traité de l'argumentation. La nouvelle rhétorique, Paris, Presses universitaires de France, 1958
• Dag Prawitz, Natural Deduction. A Proof-Theoretical Study, Stockholm, Almqvist et Wiksell, 1965
• Stephen Toulmin (trad. Philippe De Brabanter), Les Usages de l'argumentation, Paris, Presses universitaires de France, 1993

Voir aussi

• Axiome
• Déduction
• Définition
• Vérité
• Certitude
• Connaissance
• Diallèle
• Dialectique
• Argument
• A priori
• Convention
• Scepticisme
• Épistémologie
• Aristote
• René Descartes