1. Geometric theories for real number algebra without sign test or dependent choice axiom
- Author
-
Lombardi, Henri and Mahboubi, Assia
- Subjects
Mathematics - Logic ,Commutative Algebra, Mathematical Logic, Constructive Mathematics - Abstract
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, Comment: In version 4 we have fixed several typos and we give some explanations in order to best understand the construction of the 2 closure of an f-ring and of a non discrete ordered field. In this version we have improved the english translation and we have best explained the process of adding virtual roots
- Published
- 2024