Any finite extension of the rationals, along with its Galois group, can be interpreted in Peano arithmetic by straightforward means. For a fixed bound $n$ in the degree this is uniform in the coefficients of a defining polynomial so you can quantify in PA over degree (at most) $n$ extensions. As a convenient reference, http://www.logique.jussieu.fr/~zoe/papiers/Leeds08.pdf interprets degree (at most) $n$ extensions of any field in the first order theory of that field, for any concretely given $n$.

It seems to me that PA (or even in Elementary Function Arithmetic) should interpret all finite extensions of the rationals, so that we can quantify over all finite extensions and their Galois groups, by coding polynomials (and the elements of the extension defined by any given polynomial) by finite sequences.

Does that work in PA? and in EFA? Am I guilty of some ambiguity in posing the question?

Here are some details, for more see the cited paper: In PA we can interpret "for every degree three polynomial $P$" to mean just "for all numbers $s,t,u,v$," where we are going to treat these numbers as the coefficients of $P$. So this will only work for $P$ of degree three (or less), but you can code any higher fixed degree by using suitably many more variables. I take it that the step between natural number coefficients and rational number coefficients is routine and needs no explanation here.

Notably we interpret "$P$ is irreducible over the integers" as "for any degree three polynomials $Q,R$ if $Q\cdot R = P$ then either $Q$ is $0,0,0,x$ for some number $x$, or $R$ is."

Then we use Kronecker's method to interpret elements of the extension of the rationals by one root of $P$. We interpret them as also being degree two rational polynomials with addition and multiplication modulo $P$ which is obviously expressible in PA. We prove in the usual way that if $P$ is irreducible then these elements form a field. And PA can express that P has only simple roots, so it can express that this is a Galois extension. Then in this coding the four-tuple $0,0,1,0$ is a primitive element so we can interpret an element of the Galois group as root of $P$ (i.e.~the root to which $0,0,1,0$ will be taken). We just need to check that PA can express the multiplication law for the group interpreted this way, which I can add explicitly if anyone wants but perhaps it is clear now.

model$M$ interprets another model $N$ if there is a definable-in-$M$ structure consisting of tuples from $M$ which is isomorphic to $N$; see en.wikipedia.org/wiki/Interpretation_%28model_theory%29. When saying that atheoryinterprets a structure, I'm a little less sure - one possible interpretation of that is that every model of the theory interprets the structure, but that seems false, since nonstandard models of $PA$ need not (I believe) interpret, say, even $(\mathbb{Q}, +, \times)$. (cont'd) $\endgroup$4more comments