La première est que la forme écrite d'une démonstration mathématique peut être considérée comme un objet concret. Une idéologie partagée par la plupart des mathématiciens est que toute démonstration au sens usuel (écrite par des humains à destination d'autres humaines) pourrait être, au prix d'un travail fastidieux, écrite entièrement formellement à partir des axiomes de base du système logique. La correction de cette démonstration formelle peut être vérifiée par une personne stupide mais patiente, qui se contenterait de vérifier les règles de bonne formation des preuves ; ou, de façon plus pratique, par un ordinateur appliquant ces règles. C'est d'ailleurs ce travail de transformation de démonstrations pour mathématiciens en démonstrations formelles et vérifiables par ordinateur qu'accomplit mon brillant collègue Georges Gonthier (je dis « brillant » car il faut beaucoup d'intelligence pour trouver une méthode limitant l'ampleur de cette tâche afin qu'elle devienne faisable en un temps raisonnable ; ses travaux sont un véritable tour de force).

La correction d'une démonstration formalisée est alors définie par un phénomène parfaitement observable : si un algorithme (ou sa mise en œuvre dans un ordinateur) répond « oui » ou « non ».

On m'objectera que j'évoque ici la démonstrabilité des propositions et non leur vérité, concepts dont on sait bien qu'ils sont distincts depuis les travaux de Gödel. Passons donc à cette question de la vérité, soit ma seconde objection.

La vérité d'une proposition de l'arithmétique sans quantificateurs, ou avec quantificateurs bornés (∀1≤kn ⇒ ...), peut être vérifiée par un simple calcul (certes éventuellement fastidieux, mais nous avons des ordinateurs pour cela). Ceci est un phénomène observable. D'un certain point de vue, les entiers naturels (ou relatifs) sont des objets tangibles, car calculatoires.

La fausseté d'une proposition Π1 de l'arithmétique, c'est-à-dire d'une proposition de la forme ∀x1,...,∀xn F où F n'a que des quantificateurs bornés et des opérations arithmétiques, peut être vérifiée à l'aide d'un ordinateur (ou d'un calculateur humain patient) qui énumérerait tous les n-uplets x1,...,xn jusqu'à en trouver un qui viole F. De telles propositions seraient donc réfutables par un moyen physique, ce qui vérifierait le critère de Popper.

Les propositions Π1 de l'arithmétique incluent de très nombreux problèmes importants : outre, bien sûr, le problème de l'arrêt de programmes informatiques arbitraires (plus exactement : le fait pour un programme de ne pas s'arrêter), la conjecture de Goldbach, l'hypothèse de Riemann peuvent se mettre sous forme de telles propositions (voir Matiyasevich, Le dixième problème de Hilbert, §6.4).

On m'objectera que, certes, ces propositions seraient réfutables par un processus physique, mais que la conclusion de celui-ci porte sur des propriétés abstraites et non sur des propriétés du monde physique. Cependant, toute « mesure » physique suppose une part de théorie ; il en faut déjà pour construire un voltmètre à aiguille, et il en faut encore plus pour établir que le nombre affiché par un voltmètre numérique est bien la même grandeur que celle mesurée par le voltmètre à aiguille.

Il me semble que la vraie limitation est la finitude du monde physique, de la vie du calculateur humain, de la mémoire et de la vie de la machine. Il est physiquement impossible de calculer pour x1,..., xn arbitrairement grands, donc une proposition qui ne serait invalide que pour des x1,..., xn astronomiquement grands ne serait pas réfutable par ce moyen.

Cette objection me paraît cependant s'appliquer aussi bien à la physique. Celle-ci elle aussi fournit des prédictions sur des objets arbitrairement grands et pour lesquels nous ne pouvons tenter d'expériences...

Je n'ai, je l'avoue, pas cherché des ouvrages de philosophie des sciences qui éclairciraient les questions que j'ai soulevées dans ce billet. Je serais donc preneur de suggestions de lecture ou d'idées.

PS : Oui, par moment, j'ai des sympathies pour l'ultrafinitisme. Cette affirmation choquante a provoqué cette réaction de David Madore.