I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic number fields are a very restrictive subset of countable fields and will not support all the codings used in the cited paper. I suspect they will not support any codings of such flexible expressive power, and that results on algebraic number fields actually have less proof theoretic strength, but I do not know that is true. What is known about this?
For example, Dorais, Hirst, and Shafer reverse the theorem that an automorphism of an algebraic extension of countable fields extends to an automorphism of any algebraic closure of the extension. They reverse it over $\mathsf{RCA}_0$ to $\mathsf{WKL}_0$. Has anyone reversed the number field case of this?
If I am not mistaken, their Thm 8 shows $\mathsf{RCA}_0$ itself proves every automorphism of a number field $L$ extends to an automorphism of any larger Galois number field $K/L$.
There has been some thought about Galois theory of number fields in the weaker $\mathsf{RCA}^*_0$. See Reverse mathematics below RCA. Is there recent progress on that?
Is the matter sensitive to the distinction between coding algebraic number fields as extensions of $\mathbb{Q}$ which have finite bases, versus coding them as extensions with given bases?
Since many people up voted a request to clarify what reverse math is, I'll add a bit to the tag description: It is a branch of proof theory which calibrates the strength of classical mathematical theorems in terms of the axioms, typically of set existence, needed to prove them. First you show some theorem is provable in some fragment of second order arithmetic (e.g. every countable field has an algebraic closure). So the theorem is no stronger than that fragment. Then you "reverse the theorem" by showing the axioms of that fragment are actually provable from the theorem, assuming some standard base axioms. So, relative to the base axioms, the theorem is exactly as strong as the axioms of the fragment. Usually the way to reverse a theorem by coding every situation that the axiom addresses in terms of what the theorem says can be done, so the theorem itself implies whatever the axiom did. It originated in its modern form in the 1970s by H. Friedman and S. G. Simpson (see R.A. Shore, "Reverse Mathematics: The Playground of Logic", 2010).