Article body

Dans son dernier ouvrage[1], Yvon Gauthier présente son système de logique « interne » (qu’il nomme aussi logique « arithmétique », « polynomiale » et « modulaire »), dont les aspects les plus singuliers sont la négation et l’implication « locale », et l’introduction de quantificateurs « effinis ». Il donne de ce système une interprétation strictement arithmétique, d’où l’adjectif « interne », sur lequel je vais revenir. Afin de lui donner un rôle fondationnel en mathématiques, Gauthier augmente cette logique interne d’un principe de descente infinie, qu’il prend soin de distinguer de l’induction mathématique (p. 51), et il propose pour ce nouveau système, qu’il nomme « arithmétique de Fermat » (ou, à l’occasion, arithmétique « de Fermat-Kronecker » ou « polynomiale »), une preuve de consistance au chapitre 4, qui est en quelque sorte la clef de voûte du programme. Je ne peux pas juger de la validité de cette preuve. Cependant, l’ouvrage de Gauthier n’est pas dénué de philosophie : une grande partie de celui-ci est consacrée à la justification de ce programme, en référence surtout à Kronecker et au programme de Hilbert, dont il s’affiche comme une variante radicale[2]. Cette entreprise repose sur un présupposé philosophique, et c’est sur terrain que j’aimerais engager la discussion, plutôt que sur des questions « techniques », qui ne sont pas du ressort de cette revue.

Gauthier est préoccupé par des questions fondationnelles héritées du programme de Hilbert et, en philosophie, de Husserl (p. 131). Il s’agit essentiellement de trouver la théorie axiomatique qui permet de « certifier » les mathématiques et dont la justification philosophique soit satisfaisante pour l’esprit. Cependant, je crois qu’il y a eu quelque chose comme un changement de « paradigme » en théorie des démonstrations — faute d’espace, je ne parlerai que de celle-ci —, il y a de cela une trentaine d’années, entre une approche basée sur les systèmes de déduction naturelle et de calculs des séquents de Gentzen, qui ne porte plus directement sur la question des fondements, et l’approche axée sur cette question héritée de Hilbert, approche qui est basée sur ce que Dummett avait qualifié d’« analogie trompeuse avec une théorie axiomatique »[3]. Jean-Yves Girard a décrit ce changement comme le passage du « pourquoi » au « comment »[4]. Le « pourquoi » est ici la théorie de la démonstration dans son cadre hilbertien, préoccupée par le problème des fondements et par la recherche de preuves réductionnistes de consistance ; celle dont on croit par ailleurs qu’elle nous parle de l’essence des mathématiques. Le « comment » ne s’intéresse plus à cette question et consiste dans l’abandon des disputes fondationnelles afin de conserver les acquis du constructivisme, c’est-à-dire la « constructivité ». Dans le cas de l’intuitionnisme, cela veut dire qu’il faut distinguer l’idée ridicule de Brouwer de bâtir une contre-mathématique sur un fondement autre, des acquis de l’intuitionnisme sur la constructivité : l’interprétation BHK des constantes logiques et le contenu computationnel de la logique intuitionniste. La « constructivité », c’est rendre explicite l’information contenue de manière implicite dans les preuves.

En d’autres termes, dans le cadre du « pourquoi », la seule chose qui importe vraiment est l’obtention d’une preuve de consistance, c’est-à-dire la donnée d’un algorithme (algorithme d’élimination des coupures, de normalisation, etc.) dont on démontre qu’il doit terminer ; le « comment » s’intéresse aux propriétés (telles que la propriété de Church-Rosser, la complexité computationnelle, etc.) de l’algorithme en question. Ce qui explique que la méthode de substitution des termes ε, dont la preuve de terminaison « par en haut » de Ackermann pour l’arithmétique intéresse Gauthier (malgré qu’il en reconnaisse le caractère peu constructif), n’est d’aucun intérêt dans ce cadre, qui est beaucoup plus radicalement constructiviste, tout en n’étant pas « fondationnel ».

On peut prendre pour ligne de partage des eaux la fin des années soixante : c’est l’époque où la méthode de l’élimination des coupures de Gentzen a commencé à supplanter définitivement les méthodes héritées de Hilbert ; les systèmes de déduction naturelle, ignorés en dehors du contexte fondationnel des preuves de consistance, furent mis à l’ordre du jour à cette époque par Dag Prawitz, qui introduisit la méthode de normalisation des preuves[5]. C’est aussi l’époque d’un résultat charnière, l’isomorphisme de Curry-Howard entre les démonstrations en déduction naturelle intuitionniste et un lambda-calcul simplement typé[6]. Dans la foulée de ce résultat, viendront, entre autres, le système Automath de Nicolaas de Bruijn, le système F de Girard, la théorie des types intuitionniste de Martin-Löf, le calcul lambda du second ordre de Reynolds, ainsi que, dans les années quatre-vingt, les langages de programmation ML de Milner et NuPRL de Constable, le calcul des constructions Coq de Coquand & Huet et la logique linéaire de Girard. Cette dernière n’est qu’une des multiples logiques « sous-structurelles »[7], à l’instar des logiques de la pertinence, qui ont été elles aussi revitalisées dans le cadre gentzenien. En philosophie de la logique et des mathématiques, ce changement de paradigme a apporté d’importants développements, depuis le défi anti-réaliste de Prawitz et Dummett, qui reformulèrent les questions philosophiques dans le cadre du nouveau paradigme dans les années soixante-dix, jusqu’aux variantes et extensions du modèle de Dummett proposées par Wright, Tennant, Brandom, etc.

Cette liste n’a pour but que de démontrer qu’il s’agit d’une série de développements fondamentaux et incontournables du point de vue constructiviste. J’insiste sur ce dernier point, car ces développements, liés à l’implémentation sur ordinateur, sont fortement constructivistes. Gauthier, qui est toujours très bien informé, ne les ignore pas, et ceux-ci laissent leur trace dans son livre. Mais il est clair que l’isomorphisme de Curry-Howard, ni non plus les langages de programmation, ne sont pour autant au centre de ses préoccupations. Le lecteur reste perplexe lorsqu’il lit que l’isomorphisme que Gauthier propose entre polynômes et formules est « plus général » que celui entre types et formules (p. 60) et que la notion de type est « externe » (p. 115). Mais quel reproche un constructiviste peut-il honnêtement faire, par exemple, à la définition des nombres naturels dans le calcul lambda ? Par ailleurs, l’isomorphisme de Curry-Howard montre que ce n’est pas la logique intuitionniste qui est une complication jugée inutile de la logique classique, mais plutôt la logique classique, avec la règle d’élimination de la double négation qui brise la symétrie des règles d’introduction et d’élimination, ou encore par l’absence de la propriété de Church-Rosser, qui n’est pas la plus « naturelle ». Cet isomorphisme permet surtout de rendre explicite le contenu computationnel de la logique intuitionniste ; tandis que l’interprétation de la sémantique BHK en termes d’une « théorie des constructions », initiée par Kreisel, n’a pas porté fruits.

On pourra rétorquer que ces récents développements ne touchent pas véritablement les « fondements » des mathématiques. En fait, le « comment » comporte un rejet implicite de la discussion des fondements. Les doutes sur les fondements — les « doutes plus douteux que la consistance elle-même » dont parlait Kreisel — ne sont plus de mise. Par ailleurs, les disputes sur les fondements n’ont jamais résolu un problème simple, que l’on peut faire ressortir en utilisant une métaphore vestimentaire, plutôt qu’architecturale : la théorie ensembliste est comme un veston taille « très grande », et il n’est guère surprenant que les mathématiques contemporaines y entrent, mais alors se pose la question du sens des mathématiques, car l’habit ne correspond pas véritablement au personnage, tandis que les théories constructivistes sont toutes taillées un peu trop étroitement pour que les mathématiques puissent y entrer ; se pose alors la question : que faire des mathématiques dont la théorie axiomatique ne peut pas rendre compte ? Faut-il les jeter à la poubelle ? Une réponse positive semblera absurde pour la majorité silencieuse des mathématiciens, en l’absence d’autres motifs que des doutes qui sont eux-mêmes douteux. La réponse de Gauthier n’est guère satisfaisante :

A forward or progressive programme for logic and mathematics is an attempt at extending the conservative domain without relinquishing the basic principles of a foundational stance that need not be a philosophical refuge, nor a negativist attitude against non-constructivist credos. And an incitation to revisionism is meant primarily as an incentive to creative foundational work.

p. 47

Gauthier joue beaucoup sur l’opposition interne/externe, qui recoupe d’autres oppositions :

Interne ⇔ externe
arithmétique polynomiale (de Fermat) ⇔ arithmétique ensembliste (de Peano)
diagonale de Cauchy ⇔ diagonale de Cantor

Qu’advient-il des mathématiques « externes » ? La diagonale de Cantor est-elle ou non une méthode de preuve admissible en mathématiques ?

Le point de vue de Gauthier tire une grande partie de sa force du fait que la plupart des mathématiques contemporaines se situent au niveau de son arithmétique polynomiale, c’est-à-dire « en dessous » du phénomène d’incomplétude découvert par Gödel. Les résultats des programmes de Hilbert modifiés que sont la « mathématique à rebours » (reverse mathematics) de Friedman et Simpson, et la version prédicativiste de Feferman sont là pour le démontrer. Mais la signification de ses résultats reste controversée. C’est ce qu’indique par exemple le résultat de Paris et Harrington, qui montre qu’une variante finie d’un théorème de combinatoire — le théorème de Ramsey — est indécidable dans l’arithmétique de Peano, bien que toutes ses instances numériques aient une preuve, ou encore un résultat de Friedman, qui montre que l’existence des cardinaux de Mahlo permet de prouver une variante finie d’un autre théorème de combinatoire, celui de Kruskal, sur les plongements d’arbres finis. Bref, les résultats d’incomplétude de Gödel ont pour conséquence l’impossibilité de fondements finitistes. On ne peut pas, par exemple, prétendre que l’on pourrait en principe obtenir une version constructive pour toute preuve non constructive en théorie des nombres. À cela, Gauthier rétorquera probablement qu’il s’agit de résultats « externes », dans une « arithmétique ensembliste » (celle de Peano). De surcroît, pour Gauthier, les programmes de Friedman et de Feferman ratissent déjà trop large[8]. Les brèves remarques de Gauthier (p. 47) n’apportent pas de nouveaux éléments, et, malgré les nombreuses indications à propos des mathématiques récentes inspirées de Kronecker que le livre contient, le lecteur n’en retire pas une idée précise de ce qui est fondé ou non par son arithmétique polynomiale. Un programme analogue à celui de Feferman n’est-il pas souhaitable ? Et, encore une fois, qu’adviendra-il des mathématiques qui seront exclues ? Les rejeter, c’est être dogmatique, les accepter, c’est, dans le cadre du « pourquoi », poser le problème.

Pour définir ce qu’il entend par « logique interne », Gauthier se réfère à l’expression de Hilbert, « inhaltliche logische Schliessen » (p. vii, 22, 52). Pour Gauthier, « interne » réfère au « contenu », et non à un système formel externe (p. 213). On pourrait donc ajouter l’opposition suivante à celles qui précèdent :

contenu ⇔ partie formelle

Gauthier aurait pu citer ici un des premiers textes de Frege, où celui-ci contrastait son « idéographie » avec la logique de Boole :

J’y ai eu dès le début à l’esprit l’expression d’un contenu. Le point de mire de mes efforts est une lingua characterica d’abord pour les mathématiques, non un calculus limité à la pure logique. […] on peut distinguer la partie formelle […] dans le langage des mots […] de la partie proprement expressive du contenu. Les signes de l’arithmétique correspondent à la dernière. […] À l’inverse la logique symbolique de Boole ne représente que la partie formelle du langage […][9].

Dans un cas comme dans l’autre, la distinction est présentée de manière intuitive et mérite d’être définie de manière un peu plus précise. Au § 3 de son Idéographie, Frege a introduit pour cela la notion de Begrifflicher Inhalt[10]. Il est intéressant de noter que c’est entre autres en se référant à ce passage de l’Idéographie que Per Martin-Löf a élaboré la philosophie anti-formaliste qui sous-tend sa théorie intuitionniste des types[11]. Mais ce que Martin-Löf entend par « contenu » n’est pas la même chose que le « contenu » de Gauthier. Celui-ci réclame une nouvelle logique interne arithmétique, tandis que Martin-Löf utilise l’isomorphisme de Curry-Howard pour rendre explicite le « contenu » des dérivations en déduction naturelle intuitionniste grâce à des constructions dans le calcul lambda typé[12].

J’aimerais conclure par une brève remarque sur l’interprétation strictement arithmétique de la logique interne : elle ferme la porte à des échanges avec la philosophie, selon moi féconds, mais qui seraient probablement qualifiés par Gauthier d’« externes ». En effet, pour ne prendre que deux exemples, les analyses de l’assertion par Dummett[13] ont un lien étroit avec la sémantique des preuves de Gentzen — et ce lien est le coeur même de son anti-réalisme —, tandis que les jeux dialogaux de Lorenzen ont été récemment redécouverts en logique linéaire[14]. Non seulement l’idée de Lorenzen[15] était-elle simple et intuitive, mais on commence à peine de nos jours à en découvrir les vertus algébriques[16]. Celles-ci sont par ailleurs à l’origine d’un renouveau, qui se profile à l’horizon, de la logique quantique, qui avait discrètement disparu de la scène depuis une vingtaine d’années.