Re: Construction of a real closure

[Michael Barr <mbarr@math.mcgill.ca>]

John's post was interesting,  but a couple of things bother me.  Since
there are explicit enumerations of Q[x] and you can order the roots of any
polynomial by their order and adjoin the roots in order, how can you get
an uncountable closure?

Another question (for Q, although any Archimedean field should work) what
if you use Cauchy sequences generated by Newton iteration, having isolated
the real roots using Sturm and sticking to an interval in which the
derivative is positive (I am thinking of a monic polynomial that is
increasing in the end)?

Incidentally, AC doesn't bother me at all, but constructive methods are
interesting in their own right.

Michael