Relecture constructive de la théorie d'Artin-Schreier

Annals of Pure and Applied Logic 91, (1998), 59-92.
Relecture constructive de la théorie d'Artin-Schreier. pdf

Résumé :

Nous introduisons la notion de structure algébrique dynamique, inspirée de l'évaluation dynamique et de la théorie des modèles.
Nous montrons comment cette notion constructive permet une relecture de la théorie d'Artin-Schreier, avec la modification capitale que le résultat final est alors établi de manière constructive.
Nous pensons que ce que nous avons réalisé ici sur un cas d'école peut être généralisé à des parties significatives de l'algèbre classique, et est donc une contribution à la réalisation du programme de Hilbert pour l'algèbre classique.

Constructive rereading of Artin-Schreier's theory

Abstract :

We introduce the notion of "Dynamic Algebraic Structure" (DAS) inspired by Dynamic Evaluation (in computer algebra) and Model Theory. We show that this constructive notion allows a rereading of the Artin-Schreier-Robinson solution for the 17-th Hilbert Problem. So, il we know how to reread the proofs, this kind of abstract theory contains an algorithm which computes the concrete result (here, the sum of squares required by Hilbert).
Our method gives a constructive semantic for certain parts af abstract classical mathematic. The idea is the following: replace the classical algebraic structures "constructed" by Choice and Principle of Third Excluded Middle (TEM), by DAS and dynamic evaluations of these DAS. Then TEM is replaced by construction of branching in the trees of dynamic evaluation of the DAS. If Choice is used in the form of Godel completeness theorem, it is not really necessary to use it for obtaining concrete results: in DAS, Choice is simply replaced by ... nothing! This is because the classical proof is by contradiction: "if there were not a sum of squares then some formal theory would admit a pathological model".
The constructive reasoning is more direct: since the pathological theory proves 0 = 1 we know how to construct the sum of squares ... and classical models have disappeared in the proof. They are replaced by dynamic evaluations of DAS.
We think that we have given, for an academic example, a new method, realizing a kind of Hilbert Program for significative parts of classical algebra.