Constructive elementary theory of ordered fields

ps file , pdf file
with M.-F. Roy.
in: Effective Methods in Algebraic Geometry. Eds. Mora T., Traverso C.. Birkhaüser (1991).
Progress in Math. No 94 (MEGA 90), 249-262.
Version plus détaillée en français (pdf)
parue aux Publications Mathématiques de Besançon (1990)

Abstract : The classical theory of ordered fields (Artin-Schreier theory) makes intensive use of non-constructive methods, in particular of the axiom of choice. However since Tarski (and even since Sturm and Sylvester) one knows how to compute in the real closure of an ordered field K solely by computations in K. This apparent contradiction is solved in this paper.
We give here a constructive proof of the first results of the theory of ordered fields, including the existence of the real closure.
The proofs can be interpreted in the particular philosophy of each reader. In a classical point of view for example, the effective procedures in the definitions may be interpreted as given by oracles. Hence one gets the existence of the real closure of an arbitrary ordered field without the axiom of choice. In a constructive framework à la Bishop one gets the existence of the real closure of a discrete ordered field. From the point of view of classical recursive theory the proofs give uniformly primitive recursive algorithms for Turing machines with oracles.
Morevover we prove that the formal intuitionist theory of real closed discrete fields is consistant, complete, and admits TEM.
The essential tools needed are the following: a constructive version of the mean value theorem in an ordered field, the notions of prime cone and of ordered d-closed field.