Corps de l’article

Introductio. Opus et Argumentum

L’argument principal qui fait l’objet du présent débat (pour deux des co-débatteurs) est la preuve de consistance interne pour l’arithmétique de Fermat-Kronecker avec descente infinie. Cette preuve, publiée d’abord dans la revue Modern Logic, vol. 8 (2000) nos 1-2, p. 47-87, constitue le cha-pitre 4. La genèse historique de la question remonte à Fermat-Kronecker, à travers Hilbert, Poincaré et Gödel, qui avait admis la possibilité d’une preuve interne de la consistance de l’arithmétique, contrairement à ce que croit la majorité des logiciens. Cette genèse est retracée dans les chapitres 2 et 3 de l’ouvrage. Le chapitre 5 porte sur le passage de Kronecker à Brouwer. Un chapitre est consacré aux fondements de la physique chez Hilbert et sa postérité, et le chapitre final essaie de circonscrire l’état de la question fondationnelle aujourd’hui.

La version de la méthode de descente infinie que j’ai utilisée dans ma preuve est tirée de la théorie des nombres, et c’est l’arithméticien André Weil qui la caractérise le mieux à mon sens :

La descente infinie opère dans tout corps fini de nombres (idéaux ou polynômes) où le produit de deux entiers ordinaires (ou algébriques) est égal à une puissance (ou degré) et leur plus grand diviseur commun s’obtient par descente finie; c’est le cas, en particulier, pour le corps quadratique Q(?N) des formes quadratiques binaires de discriminant N.

A. Weil, Number Theory. An Approach through History, Birkhaüser, Boston, 1984, p. 335-336

C’est cette forme de la descente infinie qui s’applique à la théorie des formes (polynômes homogènes) de l’arithmétique générale de Kronecker. La théorie des formes avec indéterminées de Kronecker est fort mal connue des logiciens[2]. C’est dans la théorie polynomiale de Kronecker que j’ai immergé l’arithmétique des nombres naturels pour en démontrer la consistance interne ; le plongement s’effectue à l’aide d’une traduction polynomiale des constantes logiques qui servent de passage au principe d’équivalence des formes qui garantit à son tour l’isomorphisme arithmético-algébrique de la traduction. La décomposition polynomiale, que j’ai exhibée dans les longs calculs de l’ouvrage, correspond exactement à la descente infinie dans la suite illimitée des nombres naturels. La logique arithmétisée est ainsi totalement absorbée dans l’arithmétique polynomiale, c’est-à-dire que le contenu arithmétique absorbe la forme logique (les constantes logiques) dans les opérations arithmétiques et algébriques de la théorie des formes. La preuve de consistance n’a plus qu’à démontrer que le passage est effectif par la conclusion que (0?1) dans la décomposition polynomiale qui traduit le système formel de l’arithmétique de Fermat-Kronecker, laquelle correspond à la théorie des nombres classique. Ce système formel a des propriétés minimalistes, dont certaines sont intuitionnistes, d’autres plus radicalement constructives.

L’argument est entièrement neuf et a résisté jusqu’ici à tous les assauts. Je ne cache pas la difficulté de la question, mais une grande part de la difficulté vient de la méconnaissance, chez les logiciens en particulier, des moyens proprement mathématiques déployés dans la preuve. Au-delà des détails ou des subtilités formelles, ce qu’il faut attaquer, c’est le principe de la traduction ou de l’interprétation polynomiale « interne » de la logique dans une descente finie où l’arithmétique est auto-consistante.