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

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. s 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. cal 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. ructure 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. ll insist on the Zariski spectrum of distributive lattices and commutative rings and give a constructive interpretation of the Krull dimension. erline 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. portant facts are to be stressed. abstract proofs about points of these pointfree spaces can very often (always?) be reread as constructive proofs about constructible subsets of these spaces. , 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.