Geometric theories for real number algebra without sign test or dependent choice axiom

TL;DR

This paper develops a constructive geometric framework for real number algebra without relying on the sign test or dependent choice, aiming to describe algebraic properties and o-minimal structures in constructive mathematics.

Contribution

It introduces a dynamical geometric approach to constructively analyze real algebraic properties without classical axioms, extending to o-minimal structures.

Findings

Describes algebraic properties of real numbers constructively

Provides a framework for constructive o-minimal structures

Modifies the definition of continuous semialgebraic functions

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