2024/08/19 by Henri Lombardi, Lombardi, Henri, Assia Mahboubi +1
Computer Science · Mathematics · #Commutative Algebra #Constructive Mathematics #FOS: Mathematics #History and Theory of Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Mathematical Logic #Polynomial and algebraic computation
paper · pdf · doi:10.48550/arxiv.2408.10290
openalex publication_date 2024/08/19 · openalex created_date 2024/09/21 · openalex updated_date 2026/07/28
In this memoir, we seek to construct a constructive theory that is as complete as possible to describe the algebraic properties of the real number field in constructive mathematics without a dependent choice axiom. To this purpose, we use a dynamical version of geometric theories. We obtain a nice description of the algebraic properties of the real number field, but also a first outline for a constructive theory of certain o-minimal structures. The memoir we present here is an unfinished development of the article by the authors https://inria.hal.science/hal-01426164. Compared to that paper, however, we have modified the definition of continuous semialgebraic functions, in the same spirit in which Bishop defines a continuous real function as a uniformly continuous function on any bounded interval. Despite its unfinished nature and the many questions that we do not currently know how to answer, we hope that this paper will arouse interest for its original approach to the subject. This paper is an English translation of a French version on arXiv:2406.15218