Preservation of multiplicity of roots by $F$-morphisms between field extensions I'm trying to study basic facts of field extensions from the model-theory point of view.
Consider the language $L$ of fields, and call $at$ the family of atomic formulae. A morphism of fields is by definition an $at$-morphism of $L$-structures, that is a function $f \colon F_1 \to F_2$ such that


*

*for every $\phi(\vec{x}) \in at$, if $F_1 \models \phi(\vec{a})$
  then $F_2 \models \phi(f \, \vec{a})$.


From the theory of fields, it is known that every morphism of fields is in fact an embedding.
Let $F \subseteq E_{i = 1, 2}$ be two field extensions.
An $F$-morphism is a field morphism $f \colon F_1 \to F_2$ such that $f(x) = x$ for all $x \in F$.
In this case $f$ is an $at(F)$-morphism, where $at(F)$ is the family of atomic formulae with parameters in $F$.
For example, if $\alpha \in E_1$ is solution to a polynomial equation with coefficients in $F$, then $f(\alpha) \in E_2$ is solution to the same equation.
It is also well known that

For any set of formulae $\Delta$, every $\Delta$-embedding is a $\{\exists\}\Delta$-morphism.

Let $\alpha \in E_1$ be a root of a polynomial $p(x) \in F[x]$.
Then we can express that $\alpha$ has multiplicity at least $m$
as an $\{\exists\}\,at(F)$-formula as follows:
$$ \varphi(\alpha) \equiv \exists \, b_0, \ldots, b_s \, . \, p(x) = (x - \alpha)^m (b_s x^s + \ldots b_0)$$
where the equality of polynomials is replaced by the equality of the corresponding coefficients and $s$ is the appropriate integer.
This implies that if $\alpha \in E_1$ is a root of $p(x)$ with multiplicity $m$, then $f(\alpha) \in E_2$ is a root of $p(x)$ with multiplicity at least $m$. The intuition suggests that this multiplicity should be exactly $m$.
Whence we wish to express the property


*

*$\alpha$ has multiplicity less than or equal to $m$


with a formula that is preserved by $F$-morphisms. This seems to be expressible with a $\{\neg \exists\} \, at$-formula, or a $\{\forall\} \, at^{\pm}$-formula. But those should not be preserved by $F$-morphisms, as the following example shows:
$$\mathbb{Q} \models (\forall x \, . \, x^2 - 2 \neq 0), \qquad
\mathbb{R} \not\models (\forall x \, . \, x^2 - 2 \neq 0).$$
Questions:


*

*is the intuition of the fact that the exact multiplicity is preserved wrong?

*can this property be expressed as a formula that is preserved?

*also, is there any reference which study field extensions using model theory?


Thank you in advance.
 A: The property that $a$ is a root of $p(x)$ of multiplicity $m$ can be expressed by the following $L(F)$ formula $\varphi(a)$: $$\exists b_0,\dots,b_s\, (p(x) = (x-a)^m(b_sx^s+\dots+b_1x + b_0)\land b_sa^s+\dots+b_1a+b_0\neq 0),$$
where, as in your question, equality of polynomials is expressed by the conjunction of atomic formulas expressing equality of their coefficients. This formula says that $p(x)$ can be factored into $(x-a)^m$ times a polynomial which does not have $a$ as a root. 
$\varphi(a)$ is an existential $L(F)$ formula, and truth of existential formulas is preserved under embeddings. In general, homomorphisms only preserve the truth of positive existential formulas, and $\varphi(a)$ is not positive, because of the inequation $(b_sa^s+\dots+b_1a+b_0\neq 0)$. But as you pointed out, embeddings and homomorphisms coincide for fields. This corresponds to the fact that we can use the Rabinowitsch trick to turn inequations into equations. That is, $\varphi(a)$ is equivalent (modulo the theory of fields) to the following positive existential formula: 
$$\exists b_0,\dots,b_s,c\, (p(x) = (x-a)^m(b_sx^s+\dots+b_1x + b_0)\land (b_sa^s+\dots+b_1a+b_0)c= 1).$$
