Le point de vue constructif en mathématiques.

Ce texte au format pdf

Henri Poincaré

" M. Zermelo a voulu construire un système impeccable d'axiomes; mais ces axiomes ne peuvent être regardés comme des décrets arbitraires, puisqu'il faudrait montrer que ces décrets ne sont pas contradictoires, et qu'ayant fait entièrement table rase on n'a plus rien sur quoi l'on puisse appuyer une semblable démonstration. Il faut donc que ces axiomes soient évidents par eux-mêmes. Or quel est le mécanisme par lequel on les a construits? On a pris des axiomes qui sont vrais des collections finies; on ne pouvait les étendre tous aux collections infinies, on n'a fait cette extension que pour un certain nombre d'entre eux, choisis plus ou moins arbitrairement. A mon sens d'ailleurs [...] aucune proposition concernant les collections infinies ne peut être évidente par définition.
[...] Quant à moi je proposerais de s'en tenir aux règles suivantes:

  1. Ne jamais envisager que des objets susceptibles d'être définis en un nombre fini de mots;
  2. Ne jamais perdre de vue que toute proposition sur l'infini doit être la traduction, l'énoncé abrégé de propositions sur le fini;
  3. Éviter les classifications et les définitions non prédicatives.
[...] On se propose d'enseigner les mathématiques à un élève qui ne sait pas encore la différence qu'il y a entre l'infini et le fini; on ne se hâte pas de lui apprendre en quoi consiste cette différence; on commence par lui montrer tout ce qu'on peut savoir de l'infini sans se préoccuper de cette distinction; puis dans une région écartée du champ qu'on lui a fait parcourir, on lui découvre un petit coin où se cachent les nombres finis. Cela me paraît psychologiquement faux. ... "

Henri Poincaré, dans La logique de l'infini (Revue de Métaphysique et de Morale 1909). Réédité dans Dernières pensées, Flammarion.
Deux textes sur l'infini, en pdf. Dernières Pensées, en pdf.

C'est quoi ZFC ?

Les problèmes posés par la signification réelle des énoncés mathématiques de la théorie des ensembles (en fait théorie des ensembles infinis actuels) n'ont pas été résolus à ce jour.
Quant à la validité réelle des résultats obtenus dans cette théorie, problème de validité qui se pose lorsque les énoncés ont une signification concrète claire, elle est a priori douteuse. Et le début d'une preuve de cette validité semble hors de portée.
Que faisons-nous donc avec un système formel tel que ZFC ?
On peut affirmer comme Bourbaki qu'on joue à un jeu formel appelé "la mathématique".
C'est pourtant une option bien contestable, car quel intérêt porter à une théorie formelle dont les théorèmes ne prétendent plus énoncer des Vérités ?

Erret Bishop

Fort heureusement, une grande quantité des mathématiques produites aujourd'hui ont une signification claire, par exemple lorsqu'elles ont un contenu algorithmique incontestable.
Ainsi les bases de l'analyse moderne ont été réécrites dans ce style par Erret Bishop en 1967 dans un livre remarquable, mais passé inaperçu en France: Foundations of constructive analysis.
Le point de vue constructif en mathématiques est le point de vue "réaliste concret" qui, à propos de chaque énoncé mathématique, pose le problème de sa signification algorithmique.
Le point de vue constructif demande que toute affirmation mathématique ait un sens autre que celui d'un jeu purement formel.
Cela ne revient pas à jeter bas les mathématiques classiques mais à les aborder d'un autre point de vue.

E. Bishop, dans la préface de Foundations of constructive analysis, fait à ce sujet la remarque suivante:

" Le point de vue constructif ne signifie pas que les mathématiques classiques sont "sans valeur". Ce serait aussi stupide que de dire que d'un point de vue "classique" les mathématiques "non rigoureuses" seraient "sans valeur". Tout théorème de mathématiques classiques pose un défi au mathématicien constructif:


Vous trouverez ici, un article de Solomon Feferman, qui discute les points de vue constructifs, prédicatifs et classiques en mathématiques.

Le programme de Hilbert

Enonçons le programme de Hilbert de manière générale et informelle.

Programme de travail

  1. Lorsqu'un résultat concret est démontré en mathématiques par des méthodes douteuses, certifier ce résultat par des méthodes sûres.
  2. Réaliser ce travail de manière aussi systématique (voire automatique) que possible.

Ce programme est toujours d'actualité. Une des manières la plus efficace de le développer, c'est de faire des mathématiques constructives.
En 1985 le merveilleux petit livre de Mines, Richman et Ruitenburg A Course in Constructive Algebra a fait pour les bases de l'algèbre moderne ce qu'avait fait le livre de Bishop pour celles de l'analyse.

En fait nous devons faire face à une situation un peu paradoxale: les méthodes abstraites sont a priori douteuses, mais c'est un fait "expérimental" qu'elles ne nous trompent pas quand elles donnent un résultat de nature concrète.
Pour comprendre un tel phénomène il y a deux réactions possibles.
Ou bien on croit que les méthodes abstraites sont fondamentalement justes parce qu'elles reflètent une "réalité", une sorte d'"univers cantorien idéal" dans lequel se trouve la vraie sémantique de ZFC. C'est la position du réalisme platonicien, défendue par exemple par Gödel.
Ou bien on pense que les méthodes abstraites sont vraiment sujettes à caution. Mais alors, à moins de croire que les mathématiques relèvent de la magie ou du miracle, il faut expliquer pourquoi les mathématiques classiques se trompent si peu. Si on ne croit ni à Cantor, ni aux miracles, on est conduit à penser que les preuves abstraites de résultats concrets contiennent nécessairement des "ingrédients cachés" suffisants pour construire les preuves concrètes correspondantes.
Cette possibilité de certifier constructivement des résultats concrets obtenus par des méthodes douteuses, si on arrive à la réaliser de manière assez systématique, est dans le droit fil du programme de Hilbert.
Il faut souligner que sous cette formulation, le programme de Hilbert a déjà été confirmé pour une large partie des mathématiques usuelles, celles qui sont "codables" dans le système formel dit "de Peano": les résultats universels ou existentiels prouvés à l'aide du tiers exclu dans "Peano" peuvent également être prouvés constructivement. Plus précisément, toute fonction prouvablement récursive dans ce système formel peut être prouvée récursive sans recours au tiers exclu.
Cependant, bien qu'une grande quantité de mathématiques classiques soient codables dans "Peano", cela ne nous éclaire pas suffisamment sur le "fonctionnement des preuves classiques". Sur la manière qu'elles ont d'introduire des objets abstraits "non crédibles" pour retomber en fin de compte les pieds sur terre et nous affirmer des choses très concrètes, par exemple: oui il y a sûrement là une somme de carrés, même si je ne vous la montre pas.
Nous (pour le moment: moi et quelques complices) développons depuis quelques années une méthode, que nous espérons assez générale, pour débusquer les "ingrédients cachés" dont je parle plus haut: pour forcer la preuve classique à nous montrer sa somme de carrés.
Notre ambition est de "donner une sémantique constructive pour les mathématiques classiques usuellement pratiquées, en particulier pour les méthodes de l'algèbre abstraite".
Nous remplaçons les objets abstraits des mathématiques classiques par des spécifications incomplètes mais concrètes de ces objets. C'est la contrepartie constructive des objets abstraits.
Plus précisément nous prétendons donner une interprétation systématique de preuves classiques qui utilisent des objets abstraits en les relisant comme des preuves constructives au sujet de contreparties constructives de ces objets abstraits.
Pour plus de détails, voir Plaidoyer pour l'algèbre constructive (avec Thierry Coquand),
Le programme de Hilbert et les mathématiques constructives, et
Algèbre dynamique, espaces topologiques sans points et programme de Hilbert

Le vieux barbu

Il n'est ni nécessaire, ni suffisant, d'admirer le vieux barbu pour développer les mathématiques constructives. Néanmoins, je pense que vous trouverez comme moi ces citations intéressantes.

" Le moyen fait partie de la recherche de la vérité, aussi bien que le résultat. Il faut que la recherche de la vérité soit elle-même vraie; la recherche vraie, c'est la vérité déployée, dont les membres épars se réunissent dans le résultat. "

Karl Marx, cité par Georges Perec dans Les Choses

Et pour terminer une des fameuses "thèses sur Feuerbach":

" La question de savoir s'il y a lieu de reconnaître à la pensée humaine une vérité objective n'est pas une question théorique, mais une question pratique. C'est dans la pratique qu'il faut que l'homme prouve la vérité, c'est-à-dire la réalité, et la puissance de sa pensée, dans ce monde et pour notre temps. La discussion sur la réalité ou l'irréalité d'une pensée qui s'isole de la pratique, est purement scolastique. "