We give a general method for producing various effective Null and Positivstellensätze, and getting new Positivstellensätze in algebraically closed valued fields and ordered groups. These various effective Nullstellensätze produce algebraic identities certifying that some geometric conditions cannot be simultaneously satisfied. We produce also constructive versions of abstract classical results of algebra based on Zorn's lemma in several cases where such constructive version did not exist. For example, the fact that a real field can be totally ordered, or the fact that (...) a field can be embedded in an algebraically closed field. Our results are based on the concepts we develop of dynamical proofs and simultaneous collapse. (shrink)

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.We introduce the notion of “Dynamic Algebraic Structure” inspired by Dynamic Evaluation and Model Theory. We show that this constructive notion allows a rereading of the Artin-Schreier-Robinson solution for the 17th Hilbert Problem. So, once we know how to reread the proofs, this kind of abstract theory contains an algorithm which computes the concrete result . Our method gives a constructive semantic for certain parts of abstract classical mathematics.The idea is the following: replace the classical algebraic structures “constructed” by Choice and Principle of Third Excluded Middle , 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 significant parts of classical algebra. (shrink)

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 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 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 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 axioms.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 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 ê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. (shrink)

We study some representations of real numbers. We compare these representations, on the one hand from the viewpoint of recursive functionals, and of complexity on the other hand.The impossibility of obtaining some functions as recursive functionals is, in general, easy. This impossibility may often be explicited in terms of complexity: - existence of a sequence of low complexity whose image is not a recursive sequence, - existence of objects of low complexity but whose images have arbitrarily high time- complexity .Moreover, (...) some representations of real numbers that are equivalent from the viewpoint of recursive functionals, are very distinct from the viewpoint of complexity.We make a particular study of representations via continued fractions . We precise exactly what part of information available in the x's dfc is equivalent to the information available in its Dedekinds cut. We show that the sum of two reals whose dfcs are polynomial-time computable may be a real whose dfc has time complexity arbitrarily high.This work confirms that the unique representation of real numbers suitable for the ordinary calculus is via explicit Cauchy sequences of rationals.RésuméNous étudions différentes manières de présenter les nombres réels. Nous comparons ces présentations du point de vue des fonctionnelles récursives d'une part, et de celui des classes de complexité d'autre part.L'impossibilité d'obtenir certaines fonctions sous forme de fonctionnelles récursives est en général facile à établir. Cette impossiblité peut souvent être explicitée en termes de complexité: - il existe une suite de faible complexité dont l'image est une suite non récursive, - il existe des objets de faible complexité mais dont les images sont des objets de complexité arbitrairement grande .En outre, certaines présentations des réels équivalentes du point de vue des fonctionnelles récursives se distinguent nettement du point de vue de la complexité.Nous faisons une étude particulière concernant les développements en fraction continue . Nous précisions exactement quelle est la partie de l'information disponible dans le dfc d'un réel x qui équivaut à l'information disponible dans sa coupure de Dedekind. Nous montrons également que la somme de deux réels dont le dfc est calculable en temps polynomial peut être un réel dont le dfc est de complexité arbitrairement grande.Ce travail confirme que seule une présentation des réels via des suites de rationnels explicitement de Cauchy est adaptée aux calculs avec les réels. (shrink)

We give an elementary theory of Henselian local rings and construct the Henselisation of a local ring. All our theorems have an algorithmic content.

We give a polynomial time controlled version of a theorem of M. Hall: every real number can be written as the sum of two irrational numbers whose developments into a continued fraction contain only 1, 2, 3 or 4.

We compare two Picard groups in dimension 1. Our proofs are constructive and the results generalize a theorem of J. Sands [11].