Citation of G. C. Rota given in this paper :
Elementary though it has become after successive
presentations and simplifications, the theory of distributive lattices
is the ideal instance of a mathematical theory, where a syntax is specified
together with a complete description of all models, and what is more, a table
of semantic concepts and syntactic concepts is given, together with
a translation algorithm between the two kinds of concepts. Such an
algorithm is a ``completeness theorem''.
G. C. Rota : Indiscrete Thoughts. Birkhauser, 1995.
Abstract : We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Español and the authors. We show that the notion of Krull dimension has an explicit computational content in the form of existence (or lack of existence) of some algebraic identities. We can then get an explicit computational content where abstract results about dimensions are used to show the existence of concrete elements. This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.
Résumé :
Nous présentons des versions constructives de la théorie de la dimension
de Krull des anneaux commutatifs et des treillis distributifs.
Les fondements de ces versions constructives sont dues à
Joyal, Español et aux auteurs.
Nous montrons que la notion de dimension de Krull a un contenu
calculatoire explicite sous la forme de l'existence (ou de la non
existence) de certaines identités algébriques.
Nous pouvons alors obtenir un contenu explicite lorsque
des résultats abstraits concernant les dimensions sont utilisés
pour prédire l'existence d'objets concrets.
Ceci peut être vu comme une réalisation partielle du programme de Hilbert
pour l'algèbre commutative abstraite classique.