Vaughan Pratt and I were discussing the fundamental theorem of algebra, and we were led to some puzzles neither of us knows anything about. Let Qbar stand for the algebraic closure of the field of rational numbers. To what extent can we get our hands on Qbar in an explicit way?
(Perhaps I should say Qbar is "an" algebraic closure, since while they're all isomorphic, the full set of isomorphisms is hard to understand, and this is part of the issue.)
1) Is there a way to enumerate the elements of Qbar such that relative to this enumeration, the field operations are computable? If so, how efficiently can they be computed? If not, how far up the hierarchy of impossible-to-actually-compute functions do we have to go?
2) On the other extreme: can we even prove the existence of Qbar without the axiom of choice, or perhaps countable choice?
3) I've heard that it's even hard to get an "explicit" description of the algebraic closures of finite fields - are there any theorems to this effect?