Dear Michael, It is related to what I did, but in a different way. BTW, I remembered something incorrectly. In my J. Alg '81 paper, I actually use (not prove) Joyal's result on the existence of the real closure of an ordered field ("Cloture algebrique reelle d'un corps ordonne", Lecture, Universite de Montreal, January 1979). The proof is indeed classical, so this holds (at least) in any topos which is a BVMST (Boolean-valued-model of Set Theory), not in every topos. I show that for certain toposes E, the result is till true. I was mostly interested in toposes E which arise in sheaf represenation theorems for algebraic structures (such as von Neuman regular (differential) rings). First, I prove a general theorem for quotients T-->T* of coherent theories satisfying (what I call) the "Sturm property" in a topos E, to the effect that prime model extensions of Mod_{E}(T) in Mod_{E}(T*) exist and are preserved by continuous functors. For instance, I show that the real closure exists in toposes E = Sh_fc(B) (sheaves for finite covers in a Boolean algebra B). The example of T--->T* with T = {ordered fields} and T* = {real closed fields} is shown to have the Sturm property in E = Sh_{fc}(B) by resorting to a "mid-way-house method", first via the Gleason cover of E, and then taking its topos of double negation sheaves, which is a BVMST. By transfer, I obtain that every commutative regular f-ring (in Sets) has an (invariant, and an atomless) real closure. Another example is that of the differential closure of a differential field and a transfer to differential Von Neuman regular rings of non-zero characteristic. The question of characterizing toposes E for which a certain quotient T-->T* of coherent theories has the "Sturm property" is open. As I said, I was only interested in sheaf representations by global sections, so I only looked at such toposes. Best, Marta
I don't think this is what I was asking, although it may be related. Certainly, the context I have is one in which if you have a real closure and adjoin i, you get an algebraic closure. And the real closure is unique because it is the usual real closure. In fact, the usual real closure is used to prove some things. As I said, the construction is constructive; the proofs are classical.
Let me give an example of the flavor. Suppose you want to have a square root of a > 0. It is decidable (by hypothesis) if a > 0; what may not be decidable is whether a has a square root. What the student did (he credits Joyal with some of the main ideas, BTW, and this may be one of them) was to form F[x]/I where I is the ideal of all polynomials that vanish at sqrt(a). Even though it may not be decidable if sqrt(a) in F, it is still decidable if a polynomial vanishes there. First use Sturm's criterion to find an interval that contains exactly one root of f(x) = x^2 - a (in a real closure) and then for any polynomial g, g is in I iff gcd(f,g) has a root in that interval, again using Sturm's criterion. Clearly, F[x]/I contains a square root of a, even if it is not decidable whether that field is F.
Michael