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.