2024/06/21 by Lombardi, Henri, Mahboubi, Assia
#12D15 12J15 14Q20 14P10 03F65 03B35 #Commutative Algebra (math.AC) #FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.2406.15218
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.