[proofplan] We use [quantifier elimination for algebraically closed fields](/theorems/4310) to reduce every ring-language formula to a quantifier-free formula, uniformly over all algebraically closed fields of the fixed characteristic. Quantifier-free ring formulas are Boolean combinations of polynomial equalities, and field embeddings preserve and reflect polynomial equalities because they preserve the ring operations and are injective. Therefore every formula has the same truth value in $K$ as in $L$ after applying the embedding, which is exactly elementarity. [/proofplan]

[step:Fix an embedding between algebraically closed fields of the same characteristic] Let $p \in \{0\} \cup \{\text{prime numbers}\}$ be fixed. Let $K$ and $L$ be models of $\operatorname{ACF}_p$, and let \begin{align*} \iota: K &\to L \end{align*} be an $\mathcal{L}_{\mathrm{ring}}$-embedding. Thus $\iota$ is an injective field homomorphism preserving $0$, $1$, addition, additive inverses, and multiplication. To prove that $\iota$ is elementary, it is enough to show that for every $\mathcal{L}_{\mathrm{ring}}$-formula $\varphi(x_1,\dots,x_n,y_1,\dots,y_m)$, every tuple $a = (a_1,\dots,a_m) \in K^m$, and every tuple $b = (b_1,\dots,b_n) \in K^n$, \begin{align*} K \models \varphi(b,a) \quad \Longleftrightarrow \quad L \models \varphi(\iota(b),\iota(a)), \end{align*} where $\iota(a) := (\iota(a_1),\dots,\iota(a_m))$ and $\iota(b) := (\iota(b_1),\dots,\iota(b_n))$. [/step]

[step:Replace the formula by a quantifier-free formula using quantifier elimination]By quantifier elimination for algebraically closed fields of characteristic $p$ (citing a result not yet in the wiki: Quantifier Elimination for Algebraically Closed Fields), there exists a quantifier-free $\mathcal{L}_{\mathrm{ring}}$-formula $\psi(x_1,\dots,x_n,y_1,\dots,y_m)$ such that \begin{align*} \operatorname{ACF}_p \models \forall x_1 \cdots \forall x_n \forall y_1 \cdots \forall y_m \bigl(\varphi(x_1,\dots,x_n,y_1,\dots,y_m) \leftrightarrow \psi(x_1,\dots,x_n,y_1,\dots,y_m)\bigr). \end{align*} Since $K \models \operatorname{ACF}_p$ and $L \models \operatorname{ACF}_p$, it follows that \begin{align*} K \models \varphi(b,a) &\Longleftrightarrow K \models \psi(b,a), \\ L \models \varphi(\iota(b),\iota(a)) &\Longleftrightarrow L \models \psi(\iota(b),\iota(a)). \end{align*} Therefore it remains to prove that quantifier-free formulas are preserved and reflected by $\iota$.[/step]

[guided]The role of quantifier elimination is to remove the only part of a formula that might not be visibly respected by an arbitrary embedding: the existential and universal quantifiers. The cited theorem says that, modulo $\operatorname{ACF}_p$, every formula is equivalent to one with no quantifiers. More precisely, for the fixed formula $\varphi(x_1,\dots,x_n,y_1,\dots,y_m)$, quantifier elimination gives a quantifier-free formula $\psi(x_1,\dots,x_n,y_1,\dots,y_m)$ satisfying \begin{align*} \operatorname{ACF}_p \models \forall x_1 \cdots \forall x_n \forall y_1 \cdots \forall y_m \bigl(\varphi(x_1,\dots,x_n,y_1,\dots,y_m) \leftrightarrow \psi(x_1,\dots,x_n,y_1,\dots,y_m)\bigr). \end{align*} The hypotheses needed to use this result are exactly that $K$ and $L$ are algebraically closed fields of characteristic $p$, so both are models of $\operatorname{ACF}_p$. Hence the displayed equivalence holds inside both structures. Evaluating it at $b,a$ in $K$ and at $\iota(b),\iota(a)$ in $L$ gives \begin{align*} K \models \varphi(b,a) &\Longleftrightarrow K \models \psi(b,a), \\ L \models \varphi(\iota(b),\iota(a)) &\Longleftrightarrow L \models \psi(\iota(b),\iota(a)). \end{align*} Thus the original problem has been reduced to the quantifier-free case. This reduction is the point where algebraic closedness is used: arbitrary fields do not admit this quantifier-elimination reduction in the ring language.[/guided]

[step:Show that atomic polynomial equations are preserved and reflected] Let $t_1(x,y)$ and $t_2(x,y)$ be $\mathcal{L}_{\mathrm{ring}}$-terms in the variables $x = (x_1,\dots,x_n)$ and $y = (y_1,\dots,y_m)$. Since $\iota$ preserves the ring operations and the constants $0$ and $1$, induction on the construction of terms gives \begin{align*} \iota\bigl(t_j^K(b,a)\bigr) = t_j^L(\iota(b),\iota(a)) \end{align*} for $j \in \{1,2\}$, where $t_j^K(b,a)$ denotes the value of $t_j$ in $K$ and $t_j^L(\iota(b),\iota(a))$ denotes the value of $t_j$ in $L$. Because $\iota$ is injective, \begin{align*} t_1^K(b,a) = t_2^K(b,a) \quad \Longleftrightarrow \quad \iota\bigl(t_1^K(b,a)\bigr) = \iota\bigl(t_2^K(b,a)\bigr). \end{align*} Using the term-evaluation identity for $t_1$ and $t_2$, this becomes \begin{align*} K \models t_1(b,a) = t_2(b,a) \quad \Longleftrightarrow \quad L \models t_1(\iota(b),\iota(a)) = t_2(\iota(b),\iota(a)). \end{align*} Thus every atomic ring formula is preserved and reflected by $\iota$. [/step]

[step:Extend preservation and reflection to all quantifier-free formulas] Every quantifier-free $\mathcal{L}_{\mathrm{ring}}$-formula is obtained from atomic formulas by finitely many applications of $\neg$, $\wedge$, and $\vee$. We prove by induction on the construction of the quantifier-free formula $\theta(x,y)$ that \begin{align*} K \models \theta(b,a) \quad \Longleftrightarrow \quad L \models \theta(\iota(b),\iota(a)). \end{align*} The base case is the atomic case proved above. For the negation step, if $\theta = \neg \theta_0$, then the induction hypothesis applied to $\theta_0$ gives \begin{align*} K \models \theta_0(b,a) \quad \Longleftrightarrow \quad L \models \theta_0(\iota(b),\iota(a)), \end{align*} and taking logical negations on both sides gives the desired equivalence for $\neg \theta_0$. For the conjunction step, if $\theta = \theta_1 \wedge \theta_2$, then \begin{align*} K \models \theta(b,a) &\Longleftrightarrow \bigl(K \models \theta_1(b,a) \text{ and } K \models \theta_2(b,a)\bigr) \\ &\Longleftrightarrow \bigl(L \models \theta_1(\iota(b),\iota(a)) \text{ and } L \models \theta_2(\iota(b),\iota(a))\bigr) \\ &\Longleftrightarrow L \models \theta(\iota(b),\iota(a)), \end{align*} where the middle equivalence uses the induction hypothesis for $\theta_1$ and $\theta_2$. The disjunction step is identical with “and” replaced by “or”. Hence the equivalence holds for every quantifier-free formula. [/step]

[step:Conclude that every embedding is elementary] Apply the quantifier-free preservation result to the formula $\psi$ obtained from quantifier elimination. We get \begin{align*} K \models \psi(b,a) \quad \Longleftrightarrow \quad L \models \psi(\iota(b),\iota(a)). \end{align*} Combining this with the equivalences between $\varphi$ and $\psi$ in $K$ and in $L$ gives \begin{align*} K \models \varphi(b,a) \quad \Longleftrightarrow \quad L \models \varphi(\iota(b),\iota(a)). \end{align*} Since $\varphi$, $a$, and $b$ were arbitrary, $\iota: K \to L$ is an elementary embedding. Therefore every embedding between models of $\operatorname{ACF}_p$ is elementary, so $\operatorname{ACF}_p$ is model complete. [/step]