Théories géométriques pour l'algèbre des nombres réels sans test de signe ni axiome de choix dépendant

Abstract

In this memoir, we seek to construct a dynamical theory as complete as possible to describe the algebraic properties of the field of real numbers in constructive mathematics without axiom of dependent choice. We propose a theory which turns out to be very close to the theory of real closed local rings in classical mathematics. The theory of real closed rings is presented here in constructive form as a natural purely equational theory, which uses virtual root functions introduced in previous work. This work is also a first step through an essential goal for the future, which is to obtain a constructive version of o-minimal structures.

in French language. Version 4 add some explanations in order to best understand the 2 closure of an f-ring or of a non discreete ordered field. In this version we have best explained the process of adding virtual roots