Re: Construction of a real closure

If memory serves me, Nerode proved years ago that the necessary and sufficient condition that all the algebraic closures of a field are effectively isomorphic is that its polynomials effectively factor into irreducibles. As for the later, the ancient theorem is that if a unique factorization domain has only finitely many units and if the factorization is effective then so it is for its polynomial ring. The condition on units pretty much forces the proof.