RE: Construction of a real closure

["Marta Bunge" <martabunge@hotmail.com>]

Dear Michael,

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

Constructive methods are sometimes more than "just interesting in their own
right". If a certain theorem expressible in geometric logic can be proved
constructibly, then it is true in any topos, and so amenable to a variety of
interesting interpretations. I return to one of the examples I mentioned
from my paper ("Sheaves and prime model extensions", J. Algebra 68, 1981) to
illustrate how it works for the real closure, which has both a constructive
and a non-constructive part.


Preamble. The following theorem has been shown (Lipshitz, Trans AMS 211,
1975; van der Dries Ann. Math. 12, 1977) in order to solve the analogue of
Hilbert's 17th problem for commutative (von Neumann) regular f-rings.

Theorem. Any commutative regular f-ring has an atomless real closure.

Using the Pierce representation of any commutative (von Neumann) regular
f-ring R by an ordered field K in the (non-Boolean) topos E of sheaves on
the spectrum of K, the above theorem can be shown more easily than in the
above quoted sources, simply using the analogue for ordered fields, with
some care, since we know that, although there is an algorithm for
constructing the "real closure" of an ordered field, this does not
automatically give that such is real closed. This is how I proceed, using
the "mid-way house" method.

The inclusion F = E_{not not} >---> E factors through the Gleason cover
g:G--->E (g a surjection) via a flat inclusion i: F >---> G. Since F is a
BVM/ST, i^*g^*K >---> K' has a real closure. Thus, since i_* preserves
finitary logic, g^*K >---> i_*K' is an extension of g^*K into a real
closed field i_*K'. Sturm's theorem gives an algorithm which makes sense
in any topos, provided the ordered field one applies it to is already
contained in some real closed field.  From this follows first that g^*K
has a real closure in G, and then, by the surjectivity of g (g^*
faithful), follows that K has a real closure in E. By "transfer", the
commutative regular f-ring R ( R = \Gamma (K)) has a real closure (in
Sets).

Other results (including classically new ones) in the case of differential
rings are proved in that paper. Sheaf methods in the theory of commutative
rings are very useful in classical mathematics. See for instance "Recent
Advances in the Representation Theory of Rings and C*-Algebras by Continuous
Sections", Memoirs AMS 148, 1973. In particular, C. Mulvey, "Intuitionistic
Algebra and Representation of Rings" in that volume). Another source is
"Applications of Sheaves" (Proceedings Durham 1977), LNM 753, Springer 1977.
In particular, the papers by Fourman and Hyland, Fourman and D. Scott, and
C. Rousseau. Anyway, this is a huge subject and hints at the usefulness  of
constructive methods in algebra and analysis, when available.

Anhyway, trhis is old stuff.

Best,
Marta