Le quantificateur effini, la descente infinie et les preuves de consistance de Gauthier

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 …