Th\'eories g\'eom\'etriques pour l'alg\`ebre des nombres r\'eels sans test de signe ni axiome de choix d\'ependant

TL;DR

This paper develops a constructive dynamical theory to describe the algebraic properties of real numbers without relying on the axiom of dependent choice, aiming to approach classical real closed ring theory.

Contribution

It introduces a constructive, purely equational theory of real closed rings using virtual root functions, bridging classical and constructive mathematics.

Findings

Constructive theory closely resembles classical real closed local rings.

Uses virtual root functions to develop the theory without choice axioms.

Lays groundwork for a constructive approach to o-minimal structures.

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.