" 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:
[...]
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.
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 ?
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.
Enonçons le programme de Hilbert de manière générale et informelle.
Programme de travail
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
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. "