Interpreting the Galois theory of finite extensions of $\mathbb{Q}$ in PA

Question

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.

Answer 1

It looked straightforward to me, but proof theory can be tricky. Emil's comment convinces me I am not overlooking any pitfall here.

PA and EFA interpret the Galois groups of all finite extensions of the rationals, uniformly in the strings of coefficients of the defining polynomials. So PA and EFA can quantify over finite extensions and their Galois groups.

To clarify as requested: PA and EFA have expressions coding "$z$ is the sum (or product) of $x$ and $y$ in the extension of the rationals given by adjoining one root of polynomial $P$" and "square matrix $M$ is the multiplication table for the automorphism group of the extension given by adjoining one root of $P$." It can express when this extension is normal, and so when the automorphism group is a Galois group in the narrow sense (automorphism group of a normal separable extension). This claim of coding is justified the way the usual codings of strings and proofs etc are in proofs of G\"odel's incompleteness theorems: either numeralwise, or in terms of the extensions of formulas in the standard model.