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.