Internal Logic rassemble quelques-uns des éléments de la recherche d’Yvon Gauthier sur les fondements des mathématiques et, comme il le signale lui-même, examine à nouveau sa tentative de radicaliser le programme de Hilbert. Une radicalisation du programme de celui-ci est censée, à mon avis, prendre le point de vue finitaire de Hilbert plus au sérieux que n’ont pu le faire d’autres tentatives visant à défendre ce programme. Un tel retour aux « sources des idées métamathématiques de Hilbert » pourra, selon Gauthier, lui permettre de sauver son programme (p. 47).

La « radicalisation » de Gauthier inclut une partie positive et une partie négative. La partie négative consiste en une critique, que l’on retrouve un peu partout dans l’ouvrage, des tentatives opposées pour sauver le programme de Hilbert, en particulier des efforts visant à justifier la preuve de consistance pour l’arithmétique de Peano sur des fondements finitaires, mais aussi l’interprétation de Gödel dans Dialectica. La partie positive consiste en une présentation de la preuve de consistance de l’arithmétique au chapitre 5.

Tant la partie positive que négative du débat fondationnel du professeur Gauthier renvoient à la position qu’il défend et suivant laquelle la méthode de la descente infinie est privilégiée par rapport à celle de l’induction complète. Il s’agit-là d’un point de vue intéressant, qui est très près de la distinction entre l’infini potentiel et l’infini complet. Suivant le raisonnement axé sur la descente infinie, une proposition est dite valide pour un nombre arbitraire n en montrant que la supposition qu’elle n’est pas valide pour n implique l’existence de m < n pour laquelle elle ne vaut pas non plus. Mais puisqu’il ne peut y avoir de séquence infinie de nombres naturels descendants, cela est impossible.

La discussion du professeur Gauthier ne réussit malheureusement pas à élucider la relation qu’il croit déceler entre la descente infinie et l’induction. Le professeur Gauthier nous dit qu’un des caractères distinctifs de la descente infinie est que « it does not require a universal (classical) quantification, but [only ?] an unlimited or “effinite” quantification over indefinite, potentially infinite sequences or Brouwer’s indefinitely proceeding sequences... » (p. 57). Le quantificateur effini de Gauthier joue ici un rôle crucial.

En termes classiques, on pourrait directement formaliser le principe de la descente infinie de la manière suivante : ∀x (¬A(x) → ∃y < x ¬A(x)) → ∀x A(x). Ceci, toujours de façon classique (par contraposition du conditionnel dans l’antécédent), est équivalent à ∀x (∀y < x A(x) → A(x)) → ∀x A(x). La formalisation du professeur Gauthier qui utilise le quantificateur effini Ξ est la suivante (dans ce contexte) :

Je dois admettre que je ne suis pas en mesure de comprendre le sens de cette formule, ni de quelle manière elle constitue une formalisation du principe de la descente infinie. Ceci est peut-être imputable à ma compréhension limitée de la signification du quantificateur effini. Ξx A(x) signifie supposément que « there are effinitely many x so that A(x) » où « effinitely many » signifie « for the infinitely proceeding sequence of natural numbers ». Les scrupules finitaires du professeur Gauthier laissent croire que le quantificateur effini est une sorte de quantificateur universel finitaire, une façon de dire que A(x) est applicable à tous les nombres sans présupposer qu’il y a une totalité de nombres naturels. Si cela est admissible, on pourrait croire que le remplacement de Ξx A(x) par ∀x A(x) aboutirait à quelque chose qui serait, d’un point de vue classique, équivalent à l’induction. Cependant,

comme on peut facilement le voir, n’est pas vrai pour tous les A. D’un autre côté, dans la discussion des règles de dérivation pour le quantificateur effini (p. 87), le professeur Gauthier dit qu’il agit comme un quantificateur universel dans les occurrences positives et comme quantificateur existentiel dans les occurrences négatives. Alors, peut-être que l’équivalent classique devrait plutôt être :

Mais cela fonctionne encore plus mal, car cette proposition est fausse lorsque ∀x A(x) est faux.

À la page 81, le professeur Gauthier soutient que « from a (classical) logical point of view, infinite descent is identified with the least number principle », et, à la p. 57, après avoir introduit la version formalisée de la descente infinie, il soutient que le principe du plus petit nombre n’est équivalent à l’induction complète que d’un point de vue classique. Devons-nous alors supposer que, du point de vue de l’arithmétique de Kronecker-Fermat, la descente infinie est en quelque sorte plus près, ou peut-être même qu’elle se réduit au principe du plus petit nombre : ∃x A(x) → ∃x (A(x) ⋀ ∀y < x ¬A(x)) ? Ce qui éveille cette suspicion, c’est le fait que le principe du plus petit nombre ne contient pas de quantificateurs universels non liés du type que le professeur Gauthier juge discutable dans le schéma de l’induction complète. D’un autre côté, le professeur Gauthier semble viser une position se rapprochant de l’intuitionnisme. Pourtant, dans l’arithmétique intuitionniste, le principe d’induction est un axiome, alors que le principe du plus petit nombre ne peut pas être prouvé[1].

Peut-être que les difficultés autour du débat sur la formalisation de la descente infinie pourraient être surmontées en fournissant une sémantique et une théorie de la preuve à la logique dans laquelle, selon le professeur Gauthier, l’arithmétique de Kronecker-Fermat pourrait être fondée. C’est le but qu’il poursuit dans le chapitre 4 de son ouvrage. On pourrait s’attendre ici à une formulation précise du calcul logique, d’une sémantique, d’une preuve de consistance et peut-être même d’une preuve de complétude de la première en rapport avec cette dernière. Malheureusement, aucune de ces preuves n’est donnée. En fait, j’ai beaucoup de difficultés à comprendre la sémantique que propose le professeur Gauthier (p. 88). La notion d’une structure M semble en effet familière : un domaine D_m (en pratique, l’ensemble des nombres naturels), et les interprétations des prédicats et des symboles de fonction. Le professeur Gauthier propose ensuite une définition de la fonction ϕ_m qui assigne 0 ou 1 aux formules closes. Évidemment, ϕ_m (A) est censé donner la valeur de vérité de A. Mais la définition de ϕ est plutôt obscure. Par exemple, la formule pour la conjonction est :

Si ϕ_m est une fonction des formules de{0, 1}, alors, quel est le rôle de l’argument supplémentaire n x m ? Et que sont A_n et B_m ? Peut-être sont-ils les « valuators » auxquels le professeur Gauthier a fait allusion quelques lignes plus haut : « a number which locates the formula in the arithmetical universe ». Si A_n et B_m sont des nombres, et que D_m est la série des nombres naturels, il me semble que la partie gauche de la définition est toujours vraie — mais bien entendu toutes les conjonctions ne se voient pas assigner 1 ?

Ces défauts parmi d’autres dans la présentation des détails techniques font en sorte qu’il est difficile de cerner exactement ce que le professeur Gauthier essaie de démontrer avec sa preuve de consistance. Une fonction des formules et des preuves pour les polynômes est importante, et la descente infinie de quelques séries de polynômes est alors appliquée pour obtenir le résultat de consistance. Je soupçonne que cette approche du problème n’est pas à la base tellement différente des approches des preuves de consistance d’Ackermann et Gentzen. Eux aussi procèdent en établissant une assignation de preuves aux polynômes, mais dans leur cas, les polynômes dans lesquels ω fonctionne comme une variable et dans lesquels les exposants peuvent eux-mêmes être des polynômes. En d’autres mots, il y a une façon naturelle dans laquelle la forme normale de Cantor d’un ordinal moins que ε₀ — notation ordinale telle qu’utilisée par Gentzen et Ackermann — peut être considérée comme un polynôme. Les preuves de Gentzen et Ackermann ne nécessitent aucune sorte d’induction transfinie au sens de la théorie des ensembles. L’induction — en fait, dans ces cas, c’est la descente infinie qui est utilisée et non l’induction — procède avec de tels polynômes-ω. Le théorème de la forme normale de Cantor n’est pas du tout un « ingrédient de base » (p. 48) du travail de Gentzen et Ackermann. Le professeur Gauthier a peut-être raison de douter de l’existence des ordinaux limites <ε₀ , mais ce ne sont pas ces derniers mais bien plutôt les expressions ordinales qui jouent un rôle dans les preuves de consistance.

Ce qui est en jeu dans le débat autour du statut des preuves de consistance comme celles de Gentzen et Ackermann n’est pas de savoir s’ils utilisent ou non des objets infinitaires, c’est-à-dire des ordinaux — ils ne les utilisent évidemment pas —, mais plutôt de savoir si le finitisme a accès à l’idée qu’il n’y a pas de séquences de notations ordinales de ce type descendant infiniment. Le professeur Gauthier semble penser que cette idée ne peut pas être justifiée de manière finitaire, et l’argument (à la p. 64) semble reposer sur le fait indéniable que les « ordinaux limites » n’ont aucun prédécesseur dans l’ordre approprié. Il me semble, toutefois, qu’on peut dire la même chose des polynômes que le professeur Gauthier utilise dans sa preuve de consistance. Quel est le prédécesseur immédiat de x² + x dans l’ordre des polynômes avec lequel fonctionne sa méthode de descente infinie ? Il semble être ici face à ses polynômes dans une situation qui est tout à fait analogue à celle de Gentzen et Takeuti face aux notations ordinales. En ne fournissant pas d’explication plus précise et plus détaillée du cadre dans lequel sa preuve de consistance est développée, de même que les méthodes de preuves utilisées, il sera difficile de dissiper le doute que le caractère compliqué de sa preuve obscurcit plutôt qu’il évacue les difficultés rencontrées par la preuve de Gentzen.