[FOM] Algebraic closure of Q

[Stephen G Simpson]

Timothy Y. Chow writes:
 > The following question was motivated by a recent discussion on 
 > sci.math.research.
 > 
 > Hodges showed that ZF doesn't prove the uniqueness (up to
 > isomorphism) of an algebraic closure of Q (W. Hodges, "Lauchli's
 > algebraic closure of Q," Math. Proc. Camb. Phil. Soc. 79 (1976),
 > 289-297).
 > 
 > Question: What's really needed to prove the existence and
 > uniqueness of Qbar?  (There might be more than one answer to this
 > question.)

The existence and uniqueness of the algebraic closure of any countable
field is, of course, provable in rather weak subsystems of second
order arithmetic.  (See also the finer analysis summarized below.)
Therefore, it appears that Hodges must be talking about some other
context and/or some other sense of algebraic closure.  I am not
familiar with Hodges' result, so could you please explain the context.

Define an algebraic closure of a countable field K to be a countable
algebraically closed field L together with a monomorphism h: K --> L
such that every element of L is a root of a nonzero polynomial whose
coefficients are images under h of elements of K.  Then, the existence
of an algebraic closure of any countable field K is provable in RCA_0.
The uniqueness, up to isomorphism over K, is equivalent over RCA_0 to
WKL_0.

Define a strong algebraic closure of a countable field K to be an
algebraic closure h: K --> L as above, such that the image of K under
h exists as a subfield of L.  Then, the existence of a strong
algebraic closure of any countable field is equivalent over RCA_0 to
ACA_0.  The uniqueness is provable in WKL_0, hence in ACA_0.

See my book Subsystems of Second Order Arithmetic,
http://www.math.psu.edu/simpson/sosoa/.

--

Stephen G. Simpson
Professor of Mathematics
Pennsylvania State University
Research interests: mathematical logic, foundations of mathematics