[proofplan] We prove that any two models of $T$ satisfy the same $L$-sentences. Quantifier elimination reduces an arbitrary sentence to a quantifier-free sentence modulo $T$. Since a quantifier-free sentence contains no variables, all of its terms are closed terms, and their values lie in every $L$-substructure of a model. An isomorphism between the chosen common substructures therefore preserves the truth of the quantifier-free sentence, so the original sentence has the same truth value in both models. [/proofplan] [step:Reduce the comparison of models to quantifier-free sentences] Let $M \models T$ and $N \models T$ be arbitrary models. Let $\sigma$ be an $L$-sentence. Since $T$ has quantifier elimination, there exists a quantifier-free $L$-formula $\theta$ such that \begin{align*} T \models \sigma \leftrightarrow \theta. \end{align*} Because $\sigma$ is a sentence and $T \models \sigma \leftrightarrow \theta$, the formula $\theta$ may be taken to have no free variables; hence $\theta$ is a quantifier-free $L$-sentence. Therefore, for every model $P \models T$, \begin{align*} P \models \sigma \iff P \models \theta. \end{align*} [guided] We want to compare whether $M$ and $N$ satisfy $\sigma$. The hypothesis of quantifier elimination is exactly what allows us to remove all quantifiers from this comparison. By quantifier elimination, there is a quantifier-free $L$-formula $\theta$ such that $T$ proves, equivalently semantically entails, \begin{align*} T \models \sigma \leftrightarrow \theta. \end{align*} Since $\sigma$ has no free variables, we take $\theta$ with the same free variables as $\sigma$, namely none. Thus $\theta$ is a quantifier-free $L$-sentence. Now if $P$ is any model of $T$, then $P$ satisfies every consequence of $T$. Applying this to the displayed equivalence gives \begin{align*} P \models \sigma \iff P \models \theta. \end{align*} So it is enough to prove that $M$ and $N$ agree on the quantifier-free sentence $\theta$. [/guided] [/step] [step:Use the common substructure to preserve closed terms and atomic formulas] By hypothesis, choose $L$-substructures $A_M \subseteq M$ and $A_N \subseteq N$ and an $L$-isomorphism \begin{align*} f: A_M &\to A_N. \end{align*} Every closed $L$-term $t$ has its interpretation $t^M$ in $A_M$ and its interpretation $t^N$ in $A_N$, because $L$-substructures contain the interpretations of all constant symbols and are closed under the interpretations of all function symbols. Since $f$ is an $L$-isomorphism, induction on the construction of closed terms gives \begin{align*} f(t^M) = t^N \end{align*} for every closed $L$-term $t$. It follows that $M$ and $N$ agree on every atomic $L$-sentence. Indeed, if the atomic sentence is $t_1 = t_2$, then \begin{align*} M \models t_1 = t_2 &\iff t_1^M = t_2^M \\ &\iff f(t_1^M) = f(t_2^M) \\ &\iff t_1^N = t_2^N \\ &\iff N \models t_1 = t_2. \end{align*} If the atomic sentence is $R(t_1,\dots,t_k)$ for a $k$-ary relation symbol $R$ of $L$, then preservation of relations by the $L$-isomorphism $f$ gives \begin{align*} M \models R(t_1,\dots,t_k) &\iff (t_1^M,\dots,t_k^M) \in R^{A_M} \\ &\iff (f(t_1^M),\dots,f(t_k^M)) \in R^{A_N} \\ &\iff (t_1^N,\dots,t_k^N) \in R^{A_N} \\ &\iff N \models R(t_1,\dots,t_k). \end{align*} [guided] The important point is that a quantifier-free sentence can only talk about closed terms: terms built from constant symbols and function symbols, with no variables. These closed terms are already interpreted inside any $L$-substructure. By assumption, there are $L$-substructures $A_M \subseteq M$ and $A_N \subseteq N$ together with an $L$-isomorphism \begin{align*} f: A_M &\to A_N. \end{align*} Because $A_M$ is an $L$-substructure of $M$, it contains the interpretation of every constant symbol and is closed under every function symbol of $L$. Therefore every closed $L$-term $t$ has its value $t^M$ inside $A_M$. Similarly, $t^N \in A_N$. We now check that $f$ sends the value of each closed term in $M$ to the value of the same term in $N$. This is proved by induction on the construction of $t$. For a constant symbol $c$, preservation of constants by an $L$-isomorphism gives $f(c^M)=c^N$. If \begin{align*} t = g(t_1,\dots,t_m) \end{align*} for an $m$-ary function symbol $g$ and closed terms $t_1,\dots,t_m$, then the induction hypothesis gives $f(t_i^M)=t_i^N$ for each $i$. Since $f$ preserves the function symbol $g$, \begin{align*} f(t^M) &= f(g^M(t_1^M,\dots,t_m^M)) \\ &= g^N(f(t_1^M),\dots,f(t_m^M)) \\ &= g^N(t_1^N,\dots,t_m^N) \\ &= t^N. \end{align*} Now consider atomic sentences. For equality, the injectivity of $f$ gives \begin{align*} M \models t_1 = t_2 &\iff t_1^M = t_2^M \\ &\iff f(t_1^M) = f(t_2^M) \\ &\iff t_1^N = t_2^N \\ &\iff N \models t_1 = t_2. \end{align*} For a relation symbol $R$ of arity $k$, preservation and reflection of relations by the $L$-isomorphism gives \begin{align*} M \models R(t_1,\dots,t_k) &\iff (t_1^M,\dots,t_k^M) \in R^{A_M} \\ &\iff (f(t_1^M),\dots,f(t_k^M)) \in R^{A_N} \\ &\iff (t_1^N,\dots,t_k^N) \in R^{A_N} \\ &\iff N \models R(t_1,\dots,t_k). \end{align*} Thus $M$ and $N$ agree on every atomic $L$-sentence. [/guided] [/step] [step:Lift atomic agreement to quantifier-free agreement] The quantifier-free sentence $\theta$ is built from atomic $L$-sentences using only Boolean connectives. Since $M$ and $N$ agree on every atomic $L$-sentence, a structural induction on $\theta$ gives \begin{align*} M \models \theta \iff N \models \theta. \end{align*} Combining this with the equivalence between $\sigma$ and $\theta$ in every model of $T$, \begin{align*} M \models \sigma \iff M \models \theta \iff N \models \theta \iff N \models \sigma. \end{align*} [guided] A quantifier-free sentence is obtained from atomic sentences by finitely many Boolean operations: negation, conjunction, disjunction, implication, and equivalence, depending on the chosen logical primitives. We have already proved that $M$ and $N$ agree on the atomic sentences. A structural induction on the formula $\theta$ now proves that $M$ and $N$ agree on $\theta$. The induction step for negation uses \begin{align*} M \models \neg \varphi \iff M \not\models \varphi \iff N \not\models \varphi \iff N \models \neg \varphi. \end{align*} The induction step for conjunction uses \begin{align*} M \models \varphi \wedge \psi &\iff M \models \varphi \text{ and } M \models \psi \\ &\iff N \models \varphi \text{ and } N \models \psi \\ &\iff N \models \varphi \wedge \psi. \end{align*} The other Boolean connectives are handled by their truth-functional definitions. Therefore \begin{align*} M \models \theta \iff N \models \theta. \end{align*} Since $\sigma$ is equivalent to $\theta$ in every model of $T$, we conclude \begin{align*} M \models \sigma \iff M \models \theta \iff N \models \theta \iff N \models \sigma. \end{align*} [/guided] [/step] [step:Conclude that the theory is complete] We have shown that for every pair of models $M,N \models T$ and every $L$-sentence $\sigma$, \begin{align*} M \models \sigma \iff N \models \sigma. \end{align*} Since $T$ is satisfiable, choose a model $M_0 \models T$. For any $L$-sentence $\sigma$, either $M_0 \models \sigma$ or $M_0 \models \neg \sigma$. If $M_0 \models \sigma$, then every model of $T$ satisfies $\sigma$, so $T \models \sigma$. If $M_0 \models \neg \sigma$, then every model of $T$ satisfies $\neg \sigma$, so $T \models \neg \sigma$. Hence $T$ is complete. [/step]