[proofplan] To prove model completeness, we must show that every embedding between models of $T$ preserves all first-order formulas. Quantifier elimination reduces every formula, modulo $T$, to a quantifier-free formula. Embeddings preserve and reflect quantifier-free formulas, so the truth of the original formula is the same in the smaller model and the larger model. [/proofplan] [step:Reduce elementary preservation to quantifier-free preservation] Let $M$ and $N$ be $L$-structures such that $M \models T$ and $N \models T$, and let \begin{align*} f: M \to N \end{align*} be an $L$-embedding. We prove that $f$ is elementary. Let $\varphi(x_1,\dots,x_n)$ be an $L$-formula, and let $a_1,\dots,a_n \in M$. Write $\bar{x} := (x_1,\dots,x_n)$ and $\bar{a} := (a_1,\dots,a_n)$. By quantifier elimination, there exists a quantifier-free $L$-formula $\psi(\bar{x})$ such that \begin{align*} T \models \forall \bar{x}\,(\varphi(\bar{x}) \leftrightarrow \psi(\bar{x})). \end{align*} Since $M \models T$ and $N \models T$, this gives \begin{align*} M \models \varphi(\bar{a}) &\iff M \models \psi(\bar{a}), \\ N \models \varphi(f(\bar{a})) &\iff N \models \psi(f(\bar{a})), \end{align*} where $f(\bar{a}) := (f(a_1),\dots,f(a_n))$. Thus it remains only to prove that \begin{align*} M \models \psi(\bar{a}) \iff N \models \psi(f(\bar{a})) \end{align*} for every quantifier-free $L$-formula $\psi(\bar{x})$ and every tuple $\bar{a} \in M^n$. [/step] [step:Show that embeddings preserve and reflect quantifier-free formulas] [claim:Quantifier-free formulas are invariant under embeddings] For every quantifier-free $L$-formula $\theta(x_1,\dots,x_n)$ and every tuple $\bar{b} := (b_1,\dots,b_n) \in M^n$, \begin{align*} M \models \theta(\bar{b}) \iff N \models \theta(f(\bar{b})). \end{align*} [/claim] [proof] First we prove the corresponding statement for terms. If $t(x_1,\dots,x_n)$ is an $L$-term, then \begin{align*} f\bigl(t^M(\bar{b})\bigr) = t^N(f(\bar{b})). \end{align*} This follows by induction on the construction of $t$: variables are immediate, constants are preserved because $f$ is an $L$-embedding, and function symbols are preserved by the definition of an $L$-embedding. Now consider an atomic formula. If it has the form $t_1(\bar{x}) = t_2(\bar{x})$, then the term preservation just proved and injectivity of $f$ give \begin{align*} M \models t_1(\bar{b}) = t_2(\bar{b}) &\iff t_1^M(\bar{b}) = t_2^M(\bar{b}) \\ &\iff f(t_1^M(\bar{b})) = f(t_2^M(\bar{b})) \\ &\iff t_1^N(f(\bar{b})) = t_2^N(f(\bar{b})) \\ &\iff N \models t_1(f(\bar{b})) = t_2(f(\bar{b})). \end{align*} If the atomic formula has the form $R(t_1(\bar{x}),\dots,t_m(\bar{x}))$, where $R$ is an $m$-ary relation symbol of $L$, then term preservation and the fact that $f$ preserves and reflects $R$ give \begin{align*} M \models R(t_1(\bar{b}),\dots,t_m(\bar{b})) \iff N \models R(t_1(f(\bar{b})),\dots,t_m(f(\bar{b}))). \end{align*} Finally, every quantifier-free formula is built from atomic formulas using Boolean connectives. The equivalence is therefore preserved under $\neg$, $\wedge$, $\vee$, and the other Boolean connectives by induction on the construction of $\theta$. Hence \begin{align*} M \models \theta(\bar{b}) \iff N \models \theta(f(\bar{b})) \end{align*} for every quantifier-free $L$-formula $\theta$. [/proof] [/step] [step:Conclude that every embedding between models of $T$ is elementary] Apply the claim to the quantifier-free formula $\psi(\bar{x})$ and the tuple $\bar{a} \in M^n$. We obtain \begin{align*} M \models \psi(\bar{a}) \iff N \models \psi(f(\bar{a})). \end{align*} Combining this with the equivalences obtained from quantifier elimination gives \begin{align*} M \models \varphi(\bar{a}) &\iff M \models \psi(\bar{a}) \\ &\iff N \models \psi(f(\bar{a})) \\ &\iff N \models \varphi(f(\bar{a})). \end{align*} Since $\varphi(\bar{x})$ and $\bar{a} \in M^n$ were arbitrary, $f$ preserves and reflects every first-order $L$-formula. Therefore $f: M \to N$ is elementary. Since $M$, $N$, and $f$ were arbitrary, every embedding between models of $T$ is elementary, so $T$ is model complete. [/step]