Re: Construction of a real closure

[Peter Freyd <pjf@saul.cis.upenn.edu>]

Mike asks:

  Is there a reference for the fact that a countable decidably ordered
  field has a constructable (and decidably ordered) real closure?

The expert on all such questions is Anil Nerode .See his Effective
content of field theory (Ann. Math. Logic 17 (1979), no. 3, 289--320)
for a collection of all the relevant results.

John writes:

  Briefly, while the existence of an algebraic closure of Q
  can be shown without choice, it uniqueness-up-to-isomorphism
  seems to require choice.  Also, while arithmetic operations
  in Qbar are computable, they seem to present interesting challenges.

The need for choice could hardly arise when working with a decidable
countable structure such as  Q.

One way of naming an algebraic real number is with an ordered triple
<l, P, r>, where  l  and  r  are rationals, P  a monic polynomial with
rational coeficients that is irreducible over the rationals (the
decidablity of which can be found in van der Waerden) such that
P(l)P(r) < 0  and  R(l)R(r) > 0  for  R  any of the non-tivial iterated
derivatives of  P. Another such triple names the same element iff the
polynomials are the same and the intervals overlap. Effective
constructions for the ordered-field operations in this context are
pretty standard.