Fondements ou constructivité ?

Dans son dernier ouvrage, 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. 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 ». Jean-Yves Girard a décrit ce changement comme le passage du « pourquoi » au « comment ». 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é …