# 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).

• I don't understand what is meant by the phrase "reverse mathematics of [a collection of objects]" (as opposed to a collection of statements about objects). Can you elaborate? – Qiaochu Yuan Feb 3 '15 at 9:37
• @QiaochuYuan Perhaps I misunderstood you. Did you just want to distinguish between "reverse mathematics of algebraic number fields" and "reverse mathematics of theorems on algebraic number fields"? Reverse mathematics is always about theorems. It is like saying "proof theory of arithmetic" when you might feel it is more precise to say "proof theory for theorems of Peano arithmetic." In fact the second paragraph of the cited paper begins "Reverse mathematics of countable algebra, including topics from group theory...." – Colin McLarty Feb 3 '15 at 15:06
• @ColinMcLarty : It might help if you were to give a specific example of a statement of the form "such-and-such a result on algebraic number fields is provable in such-and-such a theory" whose status you are interested in but don't know. This is what I personally am unclear about even though I know what reverse mathematics is in general. – Timothy Chow Feb 3 '15 at 16:17
• @Colin: sorry, I was unclear. I have some sense of what reverse mathematics is in my general. My confusion is the same as Timothy Chow's; I mean what kinds of theorems about algebraic number fields do you care about? – Qiaochu Yuan Feb 3 '15 at 16:24
• "Thm 8 shows $\mathsf{RCA}_0$ itself proves every automorphism of a number field $L$ extends to an automorphism of any larger number field $K/L$." This is false. Take $L = \mathbf Q(\sqrt{2})$ and $K = \mathbf Q(\sqrt[4]{2})$. There are only two automorphisms of $K$, with the effect $\sqrt[4]{2} \mapsto \pm \sqrt[4]{2}$, and both of these fix $\sqrt{2} = \sqrt[4]{2}^2$. Therefore the nontrivial automorphism of $L$ does not extend to an automorphism of $K$. You must be leaving out a Galois hypothesis. – KConrad Apr 15 '16 at 22:39

In short, algebraic number theory flies below the radar'' of current Reverse Mathematics.
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$.
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.