Réponses à mes critiques

Je suis heureux de participer à cette nouvelle rubrique « Disputatio » dans Philosophiques. Pressé par le directeur de la revue de répondre à mes co-débatteurs, je ne peux que répliquer rapidement à la lecture cursive ou partielle de mes correspondants, pressés eux aussi de s’acquitter le plus rapidement possible de leur redevance pour une copie gratuite d’un ouvrage dispendieux, comme le laisse entendre l’un des répondants. Je répondrai à chacun en deux temps, à partir de leurs textes originaux, selon les règles de l’art médiéval auquel je voudrais modestement contribuer.

Je ne reprocherai pas aux trois co-débatteurs d’avoir négligé l’un ou l’autre des aspects essentiels de l’argumentation en faveur de la posture fondationnelle que je défends depuis plus de vingt-cinq ans (cf.Fondements des mathématiques. Introduction à une philosophie constructiviste, Montréal, PUM, 1976) et plus récemment dans le triptyque de la logique interne (à commencer par le titre inaugural De la logique interne, Paris, Vrin, 1991). Ces travaux seront complétés par La logique du contenu. Sur la logique interne en cours de publication chez l’Harmattan, Paris, 2004. Un autre ouvrage en anglais The Content of Logic. Foundations of Mathematics after Hilbert est en préparation. Je ne pourrai qu’indiquer ces textes à l’occasion dans ma réponse à la dispute. Je commence par le premier texte dans l’ordre où j’ai reçu les questions.

David DeVidi

Concedo. Il y a plusieurs fautes vénielles dans le texte publié. D. D. en relève certaines qui sont évidentes, et, parmi elles, il y a des perles et des cailloux ; les longs calculs de polynômes dans la preuve de consistance n’ont fait l’objet d’aucun reproche, typographique ou autre — je rappelle que calcul (calculus) veut dire compter des cailloux. Au moment de la réception de l’ouvrage, j’en avais fait la remarque à l’éditeur tout en ajoutant que je me consolais à l’idée que parmi les lecteurs compétents, certains passeraient outre, d’autres, moins nombreux sans doute, y trébucheraient. D. D. est parmi ceux-là, et il a trouvé des fautes apparemment moins innocentes (« innocuous » dans le texte anglais).

Respondeo. Mais il y a de plus importants glissements dans le style elliptique, les raccourcis, litotes, anacoluthes, etc. que l’alacrité de l’auteur n’a pu éviter. Je donne un exemple qui n’a pas été relevé dans un chapitre que personne ne semble avoir lu. En page 46, (chap. 2), il est écrit : « A decidable theory is consistent and finitely so ». Un lecteur perspicace (et logicien) aurait pu corriger « A decidable theory, if consistent, is finitely so ». Si subtil que soit le glissement, il a une signification pour la théorie de la décision post-hilbertienne. Mais le résultat de Hilbert, le théorème de la base finie inspiré de Kronecker, est de nature arithmético-algébrique et pré-logique, pourrait-on dire, il n’a pas besoin d’une preuve de consistance « logique ». Le point revêt une importance capitale dans le contexte de la preuve de consistance de l’arithmétique finie à l’aide de la descente infinie, une méthode de preuve que j’ai empruntée à la théorie des nombres et non à la logique ou à la théorie des démonstrations. Cela explique sans doute les irritants que dénonce D. D., qui me reproche de ne pas avoir présenté le calcul des séquents dans sa version intuitionniste. C’est pourtant une stratégie analogue qu’utilise Gentzen dans la seconde version de sa preuve de consistance de l’arithmétique ensembliste de Peano (avec induction complète) ; Gentzen écrit : « The second important distinction vis-à-vis the old concept of a derivation consists in the symmetrization of the sequents by the admission of arbitrarily many succedent formulae. This makes it unfortunately more difficult to grasp the informal sense of the various inference schemata and to persuade oneself of their “correctness” » (cf. The collected papers of Gerhard Gentzen, ed. by M. E. Szabo, North-Holland, Amsterdam, 1969, p. 259). C’est de cette auto-persuasion que D. D. a été de toute évidence incapable. J’ai plutôt présenté la version classique en supposant qu’elle était aisément réductible « en pratique » à la version intuitionniste, mais c’est la traduction polynomiale que je visais, et le calcul polynomial donne effectivement une version constructive à contenu numérique pour toute expression logique réduite à sa forme polynomiale par l’élimination des constantes logiques au profit des opérations arithmétiques sur les polynômes. Le contenu computationnel ici est une formule unique quand le polynôme comme (a’+b)ⁿ pour l’implication a une solution, qu’elle soit zéro, ou un entier quelconque dans le cas de solutions en nombre infini, comme on dit métaphoriquement ou métonymiquement. D. D. semble ici sur le seuil de comprendre ce dont il s’agit quand il parle d’une transformation arithmétique légitime. Les opérations arithmétiques et algébriques « ordinaires » et les transformations polynomiales lui apparaissent-elles suspectes ?

Mais c’est au Frege que je présente dans quatre maigres pages — p. 124-128 — dans un ouvrage de 250 pages, que D. D. s’attaque surtout. Il m’accuse de mutiler et de dénaturer le projet de Frege en le confrontant à celui de Kronecker. Tout en défendant Frege, D. D. ne manque pas de montrer les ambiguïtés de son programme. Je me contenterai de répondre ici que je prends le contre-pied de la proposition générale de Frege que je cite en page 126 de mon texte « Jusqu’où peut-on aller en arithmétique avec les seuls moyens de la logique ? » et que je renverse dans la logique arithmétique en « Jusqu’où peut-on aller en logique avec la seule arithmétique ? » Ce que j’ai voulu montrer, c’est que le programme kroneckerien réussissait pour l’arithmétique de Fermat au même titre que le programme frégéen réussit à produire une preuve de consistance à l’aide du principe de Hume et d’une théorie du deuxième ordre. Mais comme le reconnaît G. Boolos, ce n’est plus de logique mais d’arithmétique qu’il s’agit. Cela, D. D. ne peut le contester, puisqu’il condamne le logicisme au profit d’une arithmétisation de la logique, ce que réclame l’autonomie de l’arithmétique à l’intérieur de l’arithmétique, un énoncé que D. D. semble trouver incompréhensible ; c’est pourtant ce que réalise une preuve d’auto-consistance (cf. E. Nelson’s Predicative Arithmetic, Princeton University Press, 1986). Les frustrations de D. D. dans ce dernier cas touchent davantage, me semble-t-il, à son incapacité de rendre justice à Frege plutôt que de rendre compte des démérites de mon analyse. Le programme d’une logique arithmétique (ou polynomiale) est anti-frégéen ou anti-logiciste, comme je l’ai proclamé depuis De la logique interne (Vrin, 1991). Que le programme de Kronecker ait réussi là où le programme de Frege a échoué (aux mains de Frege) signifie seulement que ce dernier s’arrête sur le seuil d’une preuve d’auto-consistance. L’option philosophique, que je partage ici avec J. Hintikka et W. Goldfarb, entre autres, n’est que le reflet d’une posture fondationnelle qu’on pourrait peut-être baptiser « arithmétisme »pour les besoins de la cause.

Richard Zach

Concedo. Bien qu’il m’adresse aussi quelques reproches, R. Z. s’est rapproché plus près de ma problématique et a soulevé des questions dont certaines n’ont pas reçu de réponse suffisamment claire dans mon texte, et d’autres relèvent plus nettement d’une lecture cursive de mon ouvrage.

Respondeo. Je réponds tout de suite que toutes les questions de R. Z. ne peuvent avoir les réponses qu’il souhaite, puisqu’elles émanent de la logique classique que je récuse tout de go. Quand il veut tenter de montrer que le principe d’induction est équivalent à celui de la descente infinie par contraposition, par exemple,

(A → B) ≡ (~B → ~A),

il le fait au prix d’une double négation sur un ensemble infini (de nombres naturels). Une interprétation intuitionniste du quantificateur effini interdit le passage

~∃x ~Ax → ∀x Ax

comme tente de le faire R. Z. dans sa discussion. C’est bien pour cette raison d’ailleurs qu’on ne peut déduire le principe du plus petit nombre de l’axiome d’induction en logique intuitionniste. Cette stratégie correspond au principe du tiers exclu inadmissible dans une perspective constructiviste (p. 91). L’interprétation qu’il veut donner du quantificateur effini le réduit à un quantificateur universel classique. La lecture de R. Z. est résolument classique, et il réclame des théorèmes classiques de correction « soundness » et de complétude pour la théorie constructive que je présente, plus forte que la théorie intuitionniste des prédicats dont on sait pourtant qu’elle ne dispose pas d’un métathéorème de complétude intuitionniste.

La lecture déviante est ici la lecture classique qui suppose que l’énoncé « la suite des nombres naturels est illimitée » peut se rendre par le quantificateur universel et explique la confusion entre la version négative et la version positive expliquée en page 19 de mon ouvrage où la descente infinie correspond à un algorithme euclidien généralisé pour des équations quadratiques avec un nombre « à l’infini » de solutions que l’on ne peut « quantifier » universellement. Je suis revenu suffisamment sur la descente infinie comme algorithme euclidien généralisé dans mon texte pour insister de nouveau là-dessus. R. Z. a cependant raison de faire le rapprochement de la preuve de consistance avec les résultats de Gentzen et Ackermann pour l’arithmétique classique (de Peano) qui font appel à la seconde classe de nombres de Cantor que Hilbert avait voulu utiliser dans son essai infructueux d’une preuve de consistance finitaire. Ce que j’ai montré, c’est que le théorème de forme normale pour la seconde classe de nombres de Cantor générait un polynôme ordinal (voir p. 119). R. Zach me concède ce point, et j’avance que les formes (polynômes homogènes) avec indéterminées de Kronecker sont soumises à un principe de descente infinie ou de récessibilité uniforme que les notations ordinales ou polynômes ordinaux ne peuvent exhiber. La récessibilité uniforme est le versant descendant de l’accessibilité (Erreichbarkeit) ascendante transfinie pour la seconde classe de nombres jusqu’à l’ordinal limite  ε₀. Ce concept d’accessibilité est central chez Gentzen, et celui-ci a tenté d’en donner une justification fondationnelle en l’interprétant comme traversée potentielle « ein potentielles Durchlaufen » d’un ensemble infini. Mais la traversée potentielle se transforme en parcours actualisé de la totalité des nombres naturels dans l’induction transfinie.

La raison simple, c’est que l’induction transfinie (même restreinte aux premiers ordinaux de la hiérarchie comme dans la première version de la preuve de Gentzen), qu’on voudrait identifier (classiquement) à la descente infinie, recourt conceptuellement à un bon ordre, et il n’y a pas de suite strictement descendante pour ∠ dans un tel bon ordre. Un exemple simple, suggéré par R. Z. peut illustrer ce fait : prenons l’expression polynomiale x² + x à laquelle on assigne une valeur numérique ainsi qu’au prédécesseur immédiat x² + x – 1 ; cela donne pour un nombre naturel arbitraire : 29, 109 ou 10,099, etc. Si l’on substitue ω² + ω comme polynôme ordinal, on ne peut trouver de prédécesseur immédiat puisqu’il ne peut exister pour les ordinaux limites — on sait que dans un moment d’égarement, même Brouwer avait accepté deux ω, soit ∈ω et ω² (pour les paires de nombres naturels). L’oubli de cette circonstance mine certainement l’argument de Z. D. sur l’innocuité des notions ordinales. Soit dit en passant, la traduction polynomiale respecte les tautologies et les contradictions, p. ex. pour la conjonction

A ⋀ A ≡ A x A avec 1 x 1 ⋁ 1

et

A ⋀ ~ A ≡ A x A’ avec 1 x 0 ⋁ 0.

Un autre fait mathématique concerne le principe du plus petit nombre dont Nelson dit (cf. Predicative Arithmetic et cité dans mon texte [p. 82]) qu’il est équivalent à la descente infinie et à l’induction complète dans sa version indirecte, c’est-à-dire encore par contraposition. Je le répète, l’identification de ces trois principes repose sur l’utilisation du tiers exclu par une double négation sur un ensemble infini de nombres naturels (p. 56, 91 et sq.). Pour être bien clair, le théorème de forme normale de Cantor pour la seconde classe de nombres < ε_o, le polynôme ordinal généré par le théorème de forme normale (cf. p. 119 de mon ouvrage) et l’induction transfinie font partie du problème. La solution de Gentzen (et d’Ackermann, de Kalmar, de Takeuti et d’autres) pour la consistance de l’arithmétique de Peano a été de recourir à une technique de descente pour la réduction du degré des notations ordinales ou des polynômes ordinaux que l’on trouve déjà dans Hilbert (voir chap. 3 dans Internal Logic, qui porte sur le programme d’arithmétisation de Hilbert), et que Gentzen en particulier a voulu associer à la descente infinie dont il dit qu’elle est une forme déguisée de l’induction complète. J’ai appelé « échelle associée » la hiérarchie des ordinaux associée par Gentzen (et par Hilbert avant lui) à la suite des nombres naturels. Cette échelle associée suppose que l’on puisse atteindre ω et la suite ascendante des ordinaux > ω que l’on mettra ensuite en corrélation avec les dérivations pour réduire le degré des expressions ordinales dans la suite descendante des nombres naturels. C’est cette réduction que l’on veut identifier à la descente infinie, mais c’est une réduction ou récursion qui ne peut oblitérer le fait qu’il n’y pas de bon ordre pour < dans les suites descendantes d’ordinaux limites. Que l’on utilise une induction transfinie restreinte (aux premiers degrés transfinis) comme dans la première version de la preuve de Gentzen, ou l’induction complète sur les ordinaux, comme dans la seconde version de la preuve où l’induction transfinie devient un théorème, le problème reste entier, puisque l’induction complète sur les ordinaux est formellement équivalente à l’induction transfinie (voir Internal Logic, p. 82 et sq.). Quant à Ackermann, sa preuve de consistance de 1940 « Zur Widerspruchsfreiheit der reinen Zahlentheorie » ( Mathematische Annalen. 117, p. 162-194) ne peut se dispenser de l’induction transfinie pour la limite supérieure des indices dans les suites descendantes de nombres naturels, comme il l’admet en page 193 de son texte. C’est ce méfait logique répété à maintes reprises depuis Gentzen (par Kreisel, en particulier) que j’ai voulu corriger. Tout cela est parfaitement documenté dans mon ouvrage, et à défaut d’une lecture approfondie de l’ouvrage entier, un survol rapide des index devrait permettre de repérer les passages pertinents à toute cette discussion. Jusqu’à preuve du contraire par reductio ad absurdum qui n’est valide que dans le fini pour le constructiviste, je soutiendrai que seule la descente infinie, au sens de Fermat, c’est-à-dire la descente finie dans les nombres naturels ou au sens de Kronecker, dans l’anneau des polynômes, est justifiable dans l’arithmétique ou la théorie des nombres. Quand R. Z. s’interroge sur les méthodes de preuve que j’utilise, ce ne peut être qu’une question rhétorique, puisque tous les calculs de réduction polynomiale que j’ai effectués sont circonscrits dans la théorie de la divisibilité dans un corps fini, ce que j’ai appelé l’algorithme euclidien généralisé de la descente, ou récurrence de Fermat, dans le cadre arithmétique général de la théorie des formes de Kronecker. S’il ne l’a pas vu, c’est qu’il n’a pas regardé ou n’a pas pris le temps d’y voir ! En tout cas, R. Z. ne soulève aucune objection en ce qui touche la trame principale de la preuve. En résumé, la formulation du problème de la consistance de l’arithmétique des nombres naturels ne peut éviter la quantification effinie sur la suite illimitée des nombres naturels ; la solution du problème par descente infinie ou indéfinie, comme dit Fermat, est en réalité une descente finie, descente effectuée par décomposition polynomiale dans l’anneau des polynômes finis sans aucun ω, ce que Gentzen et alii ne peuvent accomplir pour les notations ordinales de degré ω, malgré les tentatives de justification de la démarche de Gentzen à Takeuti et jusqu’à nos jours.

Mathieu Marion

Concedo. M. M. me pose des questions plus générales sur mon travail. Ces questions, qui sont pertinentes, n’ont pas toutes leurs réponses dans l’ouvrage discuté.

Respondeo. M. M. qui connaît bien mes travaux depuis toujours (voir son compte rendu de De la logique interne dans Philosophiques, vol. XXI, n^o 1 (1994), p. 213-239), n’adhère pas totalement au point de vue constructiviste qu’il a pourtant défendu dans son ouvrage : Wittgenstein, Finitism and the Foundations of Mathematics, Oxford University Press, 1998. Son titre « Fondements ou constructivité » a une interprétation polynomiale, puisque le « ou » y devient un plus (+). C’est donc l’addition des deux termes qui constitue « les fondements constructivistes », et c’est là-dessus que je veux insister dans ma réplique.

La question la plus générale qu’il pose est la suivante : « Que fait-on des mathématiques qui n’entrent pas dans le cadre de l’arithmétique ordinaire (théorie des nombres) ou de l’arithmétique générale (algèbre polynomiale) ? ». La réponse est annoncée dans l’ouvrage et sera explicitée dans l’ouvrage à venir The Content of Logic : on loge ces mathématiques dans les extensions de l’arithmétique que je divise en extensions propres et extensions impropres. Parmi les extensions impropres, je place l’arithmétique transfinie de Cantor, l’arithmétique p-adique et surtout l’analyse p-adique qui peut se servir de la diagonale de Cantor pour obtenir les complétés de Q, le corps des nombres rationnels. Les extensions propres, comme la géométrie arithmétique (ou la partie arithmétique de la géométrie algébrique) relèvent de l’arithmétique générale (allgemeine Arithmetik) au sens de Kronecker, comme je l’ai bien montré dans mon ouvrage. C’est dans ce contexte que je peux répondre à une autre question de M. M. : la méthode de la diagonale de Cantor ne fait pas partie de la théorie (arithmétique) des nombres ni de la théorie algébrique des nombres — comme l’a montré A. Weil dans son ouvrage Basic Number Theory au grand dam de certains logiciens —, mais elle peut faire partie de la théorie analytique des nombres, en particulier de la théorie des nombres transcendants comme méthode transcendante de démonstration. Mais là encore on a des résultats d’approximation logarithmique (Baker) qui réduisent la transcendance, si l’on peut dire.

Un résultat récent qui tombe naturellement dans le cadre arithmétique, et plus précisément dans la matrice de la logique polynomiale modulaire que j’ai esquissée dans mon ouvrage (pp. 193-201), est le résultat récent d’Agrawal et alii sur la factorisation des nombres premiers en temps polynomial par un algorithme déterministe, « PRIMES is in P » ; ce résultat spectaculaire qui n’était pas connu lors de la publication d’Internal Logic utilise une version polynomiale du « petit » théorème de Fermat sur les congruences modulo, un nombre premier que j’ai évoqué dans mon livre (p. 198) — ici aussi deux fautes de frappe doivent être corrigées, — un petit a pour un grand A et un n pour un p ! Des précisions là-dessus et bien d’autres choses, comme les logiques substructurales et l’isomorphisme « externaliste » de Curry-Howard, se trouvent dans l’ouvrage sous presse La logique du contenu, chez l’Harmattan, qui peut apparaître à la fin comme un complément de l’ouvrage discuté et dans lequel j’obtiendrai peut-être le pardon pour les fautes vénielles commises dans l’ouvrage publié chez Kluwer.

Conclusio

J’estime avoir répondu en bonne partie aux objections soulevées dans les lectures partielles (je ne dis pas partiales) de mon texte qui se sont attachées à l’analyse du chapitre 4 d’Internal Logic, la preuve de consistance interne de l’arithmétique à l’aide de la descente infinie. La première mouture de la preuve remonte à 1993 : le texte a été soumis en 1995 à Modern Logic, qui l’a finalement publié en 2000. Elle a été reprise avec corrections mineures dans Internal Logic avant de paraître en français dans un livre La logique interne. Modèles et applications, Paris/Montréal, Diderot Modulo, 1997. Les aléas de la publication ne sont pas sans rappeler les avatars de la preuve de Gentzen pour l’arithmétique de Peano, qui a connu plusieurs remaniements. Je l’ai peaufinée encore dans l’ouvrage en cours de publication chez l’Harmattan et dans un autre ouvrage en anglais, The Content of Logic, pour en éradiquer les scories formelles et informelles ; la présente « disputatio » aura sans doute contribué à clarifier les enjeux d’une preuve qui dans sa nouveauté radicale ne peut manquer de susciter la controverse ou le scepticisme chez d’aucuns. L’approbation ou l’« appreuve » de la preuve ne peut se faire sans débat. J’espère seulement n’avoir pas faussé le sens du débat en y contribuant — sans mimer le cocher trop agacé par la mouche du coche — avec une certaine ardeur polémique, ce qui n’est pas incompatible avec la posture constructiviste comme l’ont montré par le passé Kronecker, Brouwer ou plus récemment Bishop. Faut-il conclure le débat avec les mots de Cicéron qui peuvent caractériser l’auteur (et peut-être aussi chacun des co-débatteurs) : « Mediocris in dicendo, doctissimus in disputando » ?