Erratum : Pour la référence [37], dans l'article paru à Annals of Pure and Applied Logic, il manque un des trois auteurs: Ihsen Yengui.
Résumé :
Une manière pertinente de revisiter le Programme de Hilbert
serait la suivante:
donner une sémantique constructive
pour les mathématiques classiques.
Plus précisément
donner une interprétation systématique des
preuves classiques abstraites
(qui utilisent le principe du tiers exclu et
l'axiome du choix) au sujet des objets abstraits,
en terme de preuves constructives au sujet de contreparties
constructives de ces objets abstraits.
Si ce programme est rempli, nous sommes capables
à la fin de l'histoire d'extraire des preuves constructives
de résultats concrets à partir des preuves
classiques abstraites de ces résultats.
Les structures algébriques dynamiques,
ou ce qui revient à peu près au même les
théories géométriques, semblent
être un bon outil pour réaliser ce travail.
Dans cette optique, les objets abstraits des mathématiques
classiques sont remplacés par des
spécifications incomplètes mais concrètes
de ces mêmes objets.
La structure des théories géométriques
donne naissance
de manière naturelle à des treillis distributifs et à
des espaces
topologiques sans points.
Les objets abstraits utilisés par les mathématiques
classiques correspondent aux points classiques
de ces espaces sans points.
Il faut insister sur deux faits expérimentaux importants.
1) Les preuves abstraites au sujet des points
de ces espaces sans points peuvent en général (toujours?)
être relues comme des preuves concernant les
parties constructibles de ces espaces
2) Les espaces de fonctions continues
sur ces espaces sans points sont souvent utilisés
dans d'élégantes théories abstraites.
Ces espaces de fonctions sont bien définis constructivement.
Cela tient au théorème de compacité
qui nous dit que
dans le cadre en question tout est fini.
La relecture constructive des preuves abstraites
n'est alors rien d'autre que la constatation que
les axiomes géométriques sont utilisés
de manière correcte.
Abstract :
A possible relevant meaning of Hilbert's program is the following one:
give a constructive semantic for classical mathematics.
More precisely, give a systematic interpretation of classical abstract
proofs (that use Third Excluded Middle and Choice) about abstract objects,
as constructive proofs about constructive versions of these objects.
If this program is fulfilled we are able
at the end of the tale to extract constructive proofs
of concrete results from classical abstract proofs of these results.
Dynamical algebraic structures or
(this is more ore less the same thing) geometric theories
seem to be a good tool for doing this job.
In this setting, classical abstract objects are
interpreted through incomplete concrete specifications
of these objects.
The structure of axioms in geometric theories give
rise in a natural way to distributive lattices and
pointfree topological spaces.
Abstract objects correspond to classical points
of these pointfree spaces.
Two important experimental facts are to be stressed:
1) Abstract proofs about points of these pointfree
spaces can very often (always?) be reread as constructive
proofs about constructible subsets of these spaces
2) Function spaces on these pointfree spaces are
often explicitely used in elegant abstract theories.
The structure of these function spaces is fully constructive:
indeed by compactness theorem, all is finite.
The constructive rereading of the abstract proofs
is in this setting is nothing but the simple constatation
that abstract proofs use correctly (geometric) axioms.