Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert

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.Dans cet article, nous illustrerons ce phénomène principalement avec le spectre de Zariski des treillis distributifs et celui des anneaux commutatifs, en indiquant notamment un équivalent constructif de la notion de dimension de Krull.Nous insistons sur le caractère extrêmement général de l’interpétation des objets abstraits idéaux des mathématiques classiques comme des points d’espaces spectraux associés à des treillis distributifs qui sont définis de façon naturelle et concrète.Souligons deux faits d’expérience importants.Tout d’abord, 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.Enfin, 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.

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 or 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 gives rise in a natural way to distributive lattices and pointfree topological spaces. Abstract objects correspond to classical points of these pointfree spaces.We shall insist on the Zariski spectrum of distributive lattices and commutative rings and give a constructive interpretation of the Krull dimension.We underline the fact that many abstract objects in classical mathematics can be viewed as points of spectral spaces corresponding to distributive lattices whose definition is concrete and natural.Two important facts are to be stressed.First, abstract proofs about points of these pointfree spaces can very often (always?) be reread as constructive proofs about constructible subsets of these spaces.Second, function spaces on these pointfree spaces are often explicitly used in elegant abstract theories. The structure of these function spaces is fully constructive: indeed by the 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.