zbMATH — the first resource for mathematics

Elementary constructive theory of ordered fields. (English) Zbl 0732.12002
Effective methods in algebraic geometry, Proc. Symp., Castiglioncello/Italy 1990, Prog. Math. 94, 249-262 (1991).
[For the entire collection see Zbl 0721.00009.]
It is proved that it is possible to construct the real closure of an ordered field without using the axiom of choice. This is not surprising since the real closure is uniquely ordered, and hence there are no possible automorphisms. One basic reason for this result is the fact that the number of real roots in the real closure is fixed by Sturm’s theorem and is given by an effective method.
The main technical difficulty is that one does not know the existence of a real closed field containing the given ordered field. The proof proceeds by induction and consists in adding carefully the needed roots of the polynomials of degree smaller than d. An antique version of the result can be found in A. Hollkott’s thesis [Finite construction of ordered algebraic extensions of ordered fields (German) (Hamburg, 1941; Zbl 0026.19801)].
Reviewer: M.-F.Roy (Rennes)

12D15 Fields related with sums of squares (formally real fields, Pythagorean fields, etc.)
12J15 Ordered fields
03F60 Constructive and recursive analysis