One can show that the statement that every field has an algebraic closure requires the axiom of choice.
However, for almost all "everyday" fields, it seems that one can actually produce an algebraic closure quite explicitly without using AC (by which I mean: one can produce an algebraic extension of the base field, and prove that it is algebraically closed, without using AC). One cannot necessarily prove the uniqueness of the algebraic closure, but one can nevertheless construct one. For instance:
- Finite fields;
- Fields of formal Laurent series over an algebraically closed field (the algebraic closure being given by the field of Puiseux series);
- The field of rational functions over an algebraically closed field: it embeds in the field of formal Laurent series, so one can take its algebraic closure in the field of Puiseux series. More generally, any subfield of a field whose algebraic closure exists in ZF also has an algebraic closure in ZF.
- The real numbers. This one I am only 95% sure about. One can obviously construct $\mathbf C$ from $\mathbf R$ without choice, but all of the proofs that $\mathbf C$ is algebraically closed use analysis in some way, and perhaps things might go wrong here. (The analytic input in Legendre's proof that $\mathbf C$ is algebraically closed seems to be only the intermediate value theorem, which doesn't depend on AC. Nevertheless, I'd be happy if an expert could chime in!)
- $\mathbf Q$. If (5) is indeed true, then one can construct the algebraic closure of $\mathbf Q$ without AC by taking the algebraic closure of $\mathbf Q$ in $\mathbf C$. Alternatively, and more simply, one can also do this directly by writing down an enumeration of $\mathbf Q[x]$.
- $\mathbf Q_p$. This one I am not completely sure about either. One can use Krasner's lemma to prove that $\mathbf Q_p$ has finitely many extensions of a given degree up to isomorphism, and one should be able to use this to write down a countable subset of $\mathbf Q_p[x]$ whose splitting field is an algebraic closure of $\mathbf Q_p$. But perhaps I am missing a subtle point.
Question: Does there exist an explicit example of a field the existence of whose algebraic closure can be proven to depend on AC? A natural candidate might be a field of rational functions in a very large number of variables. However, the less "degenerate" the example is, the better!