What is known about the reverse mathematics of algebraic number fields? 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).
 A: In short, algebraic number theory ``flies below the radar'' of current Reverse Mathematics.  
First, after working on this a while, I think it is fair to say most familiar theorems on algebraic number fields that do not refer to the algebraic closure, or real closure, of the rationals are provable in EFA, exponential function arithmetic.  (This is roughly because polynomials are themselves finite sequences of coefficients, and EFA gives an adequate theory of finite sequences.)
Second, the answer by Bjørn Kjos-Hanssen to What is the reverse mathematical strength of the fundamental theorem of algebra? notes that Tanaka and Yamazaki have proved the fundamental theorem of algebra as well as quantifier elimination for the theory of real closed fields in $\mathrm{RCA}_0$.
So the reverse mathematics of these topics lies below the base theory of most of Reverse Mathematics today.  On one hand, reverse math results about this will await the creation of a reverse math over EFA.  
On the other hand, provability (without reversals) of various theorems that deal with the algebraic or real closures of $\mathbb{Q}$ can be explored now by catch as catch can methods.  
