[proofplan] We first prove a stronger preservation statement: every formula is preserved by every finitely generated partial isomorphism satisfying the given back-and-forth hypotheses. The proof is by induction on formula complexity, with the existential step using the extension property to move a witness across the partial isomorphism. Then tuples with the same quantifier-free type have the same complete type in all models of $T$. Finally, the first-order [compactness theorem](/theorems/2748) converts this semantic preservation criterion into an actual quantifier-free formula equivalent to any given formula modulo $T$; the compactness theorem is used as a metatheorem here (citing a result not yet in the wiki: [Compactness Theorem for First-Order Logic](/theorems/4290)). [/proofplan]

[step:Prove that partial isomorphisms preserve all formulas]Let $M,N \models T$. Let $A \subset M$ and $B \subset N$ be finitely generated $L$-substructures, and let \begin{align*} f: A \to B \end{align*} be an $L$-substructure isomorphism. We prove by induction on the complexity of an $L$-formula $\varphi(x_1,\dots,x_n)$ that for every tuple $a = (a_1,\dots,a_n) \in A^n$, \begin{align*} M \models \varphi(a_1,\dots,a_n) \quad \Longleftrightarrow \quad N \models \varphi(f(a_1),\dots,f(a_n)). \end{align*} For atomic formulas, this follows from the definition of an $L$-substructure isomorphism: terms evaluated at $a$ remain inside $A$, the map $f$ commutes with all function symbols, and $f$ preserves equality and all relation symbols. Boolean connectives are immediate from the induction hypothesis and the truth definitions for $\neg$, $\wedge$, and $\vee$. It remains to treat existential formulas. Suppose \begin{align*} \varphi(x_1,\dots,x_n) := \exists y\, \theta(x_1,\dots,x_n,y). \end{align*} Assume first that $M \models \exists y\,\theta(a_1,\dots,a_n,y)$. Choose $c \in M$ such that \begin{align*} M \models \theta(a_1,\dots,a_n,c). \end{align*} By the forward extension property, there exist $d \in N$ and an isomorphism \begin{align*} g: \langle A \cup \{c\} \rangle_M \to \langle B \cup \{d\} \rangle_N \end{align*} such that $g|_A = f$ and $g(c)=d$. Since $\theta$ has lower complexity than $\varphi$, the induction hypothesis applied to $g$ gives \begin{align*} N \models \theta(f(a_1),\dots,f(a_n),d). \end{align*} Therefore \begin{align*} N \models \exists y\,\theta(f(a_1),\dots,f(a_n),y). \end{align*} The reverse implication is identical with the roles of $M,A,c$ and $N,B,d$ exchanged, using the backward extension property. Hence $f$ preserves $\varphi$.[/step]

[guided]The induction statement is deliberately stronger than merely saying that quantifier-free agreement implies full agreement. We keep an actual isomorphism \begin{align*} f: A \to B \end{align*} between finitely generated substructures in the background, because the existential step needs to enlarge the domain by a witness. For an atomic formula, there are only two things to check. First, if $t(x_1,\dots,x_n)$ is an $L$-term and $a \in A^n$, then $t^M(a) \in A$ because $A$ is an $L$-substructure of $M$. Second, since $f$ is an $L$-substructure isomorphism, \begin{align*} f(t^M(a)) = t^N(f(a)). \end{align*} Thus equality of terms and membership in relation symbols are preserved exactly. This proves the atomic case. The Boolean cases follow because satisfaction of $\neg \theta$, $\theta_1 \wedge \theta_2$, and $\theta_1 \vee \theta_2$ is defined purely in terms of satisfaction of the smaller formulas. Now consider the only genuinely model-theoretic step: \begin{align*} \varphi(x_1,\dots,x_n) := \exists y\,\theta(x_1,\dots,x_n,y). \end{align*} Assume \begin{align*} M \models \exists y\,\theta(a_1,\dots,a_n,y). \end{align*} This means that there is a concrete witness $c \in M$ with \begin{align*} M \models \theta(a_1,\dots,a_n,c). \end{align*} The current partial isomorphism $f: A \to B$ may not contain $c$ in its domain, so we cannot apply the induction hypothesis yet. The forward extension property fixes exactly this problem: it gives an element $d \in N$ and an isomorphism \begin{align*} g: \langle A \cup \{c\} \rangle_M \to \langle B \cup \{d\} \rangle_N \end{align*} with $g|_A=f$ and $g(c)=d$. Now the tuple $(a_1,\dots,a_n,c)$ lies in the domain of $g$, and $\theta$ is simpler than $\exists y\,\theta$. Therefore the induction hypothesis applied to $g$ gives \begin{align*} N \models \theta(f(a_1),\dots,f(a_n),d). \end{align*} Since $d \in N$ is a witness, this implies \begin{align*} N \models \exists y\,\theta(f(a_1),\dots,f(a_n),y). \end{align*} The converse direction uses the second extension property in the same way: start with a witness $d \in N$, extend backward to a witness $c \in M$, and apply the induction hypothesis to the extended isomorphism.[/guided]

[step:Convert quantifier-free agreement into full elementary agreement]Let $M,N \models T$ and let $a=(a_1,\dots,a_n) \in M^n$, $b=(b_1,\dots,b_n) \in N^n$. Suppose that $a$ and $b$ satisfy the same quantifier-free $L$-formulas. Let $\langle a \rangle_M$ denote the $L$-substructure of $M$ generated by $\{a_1,\dots,a_n\}$, and let $\langle b \rangle_N$ denote the $L$-substructure of $N$ generated by $\{b_1,\dots,b_n\}$. Define \begin{align*} f: \langle a \rangle_M &\to \langle b \rangle_N \end{align*} by \begin{align*} f(t^M(a_1,\dots,a_n)) := t^N(b_1,\dots,b_n) \end{align*} for every $L$-term $t(x_1,\dots,x_n)$. This map is well-defined because if $t^M(a)=s^M(a)$, then $M \models t(x)=s(x)$ at $a$, so $N \models t(x)=s(x)$ at $b$, and hence $t^N(b)=s^N(b)$. The same quantifier-free agreement shows that $f$ preserves and reflects all relation symbols, and the definition shows that it commutes with all function symbols. Thus $f$ is an isomorphism of finitely generated $L$-substructures. By the previous step, $f$ preserves every $L$-formula. Therefore for every $L$-formula $\varphi(x_1,\dots,x_n)$, \begin{align*} M \models \varphi(a_1,\dots,a_n) \quad \Longleftrightarrow \quad N \models \varphi(b_1,\dots,b_n). \end{align*}[/step]

[guided]The purpose of this step is to remove the explicit partial isomorphism from the statement. Suppose $a \in M^n$ and $b \in N^n$ agree on every quantifier-free formula. We build the only possible isomorphism between the substructures they generate: a term value in $\langle a\rangle_M$ is sent to the corresponding term value in $\langle b\rangle_N$. The possible obstruction is well-definedness. The same element of $\langle a\rangle_M$ may be represented by two different terms. If \begin{align*} t^M(a_1,\dots,a_n) = s^M(a_1,\dots,a_n), \end{align*} then the quantifier-free formula $t(x_1,\dots,x_n)=s(x_1,\dots,x_n)$ holds of $a$ in $M$. By quantifier-free agreement, it holds of $b$ in $N$, so \begin{align*} t^N(b_1,\dots,b_n) = s^N(b_1,\dots,b_n). \end{align*} Thus the definition of $f$ does not depend on the chosen term representative. The same argument handles relation symbols. If $R$ is an $m$-ary relation symbol of $L$ and $u_1,\dots,u_m$ are elements of $\langle a\rangle_M$, choose $L$-terms $t_1,\dots,t_m$ such that $u_i=t_i^M(a)$. Then \begin{align*} M \models R(t_1(a),\dots,t_m(a)) \end{align*} if and only if \begin{align*} N \models R(t_1(b),\dots,t_m(b)), \end{align*} because this is a quantifier-free formula. Hence $f$ preserves and reflects $R$. Function symbols are preserved by construction, since applying a function symbol to term values gives another term value. Therefore $f$ is an isomorphism between finitely generated substructures, and the preservation result from the previous step applies to every formula.[/guided]

[step:Use compactness to extract a quantifier-free equivalent]Fix an $L$-formula $\varphi(x_1,\dots,x_n)$. Let $\mathcal Q_\varphi$ be the set of quantifier-free $L$-formulas $\theta(x_1,\dots,x_n)$ such that \begin{align*} T \models \forall x_1\cdots \forall x_n\,(\theta(x_1,\dots,x_n) \to \varphi(x_1,\dots,x_n)). \end{align*} We first show that every realization of $\varphi$ in a model of $T$ satisfies some formula in $\mathcal Q_\varphi$. Let $M \models T$ and $a \in M^n$ with $M \models \varphi(a)$. Let $p_{\mathrm{qf}}(a)$ be the set of all quantifier-free $L$-formulas true of $a$ in $M$. If \begin{align*} T \cup p_{\mathrm{qf}}(a) \cup \{\neg \varphi(x_1,\dots,x_n)\} \end{align*} were satisfiable, then there would be a model $N \models T$ and a tuple $b \in N^n$ with the same quantifier-free type as $a$ but with $N \models \neg\varphi(b)$. This contradicts the previous step. Hence this set is inconsistent. By the compactness theorem for first-order logic, there are quantifier-free formulas $\eta_1,\dots,\eta_m \in p_{\mathrm{qf}}(a)$ such that \begin{align*} T \models \forall x_1\cdots\forall x_n\,\bigl((\eta_1 \wedge \cdots \wedge \eta_m) \to \varphi\bigr). \end{align*} Thus the quantifier-free formula \begin{align*} \theta_a := \eta_1 \wedge \cdots \wedge \eta_m \end{align*} belongs to $\mathcal Q_\varphi$ and satisfies $M \models \theta_a(a)$. Now suppose the set \begin{align*} T \cup \{\varphi(x_1,\dots,x_n)\} \cup \{\neg\theta(x_1,\dots,x_n) : \theta \in \mathcal Q_\varphi\} \end{align*} were satisfiable. Then some model $M \models T$ would contain a tuple $a \in M^n$ satisfying $\varphi$ but satisfying no formula in $\mathcal Q_\varphi$, contradicting the preceding paragraph. Therefore this set is inconsistent. By compactness again, there exist $\theta_1,\dots,\theta_r \in \mathcal Q_\varphi$ such that \begin{align*} T \models \forall x_1\cdots\forall x_n\,\bigl(\varphi \to (\theta_1 \vee \cdots \vee \theta_r)\bigr). \end{align*} Since each $\theta_i$ belongs to $\mathcal Q_\varphi$, we also have \begin{align*} T \models \forall x_1\cdots\forall x_n\,\bigl((\theta_1 \vee \cdots \vee \theta_r) \to \varphi\bigr). \end{align*} Set \begin{align*} \psi := \theta_1 \vee \cdots \vee \theta_r. \end{align*} Then $\psi$ is quantifier-free and \begin{align*} T \models \forall x_1\cdots\forall x_n\,(\varphi \leftrightarrow \psi). \end{align*} Since $\varphi$ was arbitrary, $T$ has quantifier elimination.[/step]

[guided]The semantic preservation result says that quantifier-free information determines all first-order information in models of $T$. To turn this into quantifier elimination, we must produce an actual quantifier-free formula equivalent to a given formula $\varphi$. Define $\mathcal Q_\varphi$ to be the collection of all quantifier-free formulas that already imply $\varphi$ modulo $T$. Thus a formula $\theta(x_1,\dots,x_n)$ lies in $\mathcal Q_\varphi$ exactly when \begin{align*} T \models \forall x_1\cdots \forall x_n\,(\theta \to \varphi). \end{align*} We claim first that every tuple satisfying $\varphi$ satisfies at least one member of $\mathcal Q_\varphi$. Let $M \models T$ and $a \in M^n$ satisfy $M \models \varphi(a)$. Let $p_{\mathrm{qf}}(a)$ denote the complete quantifier-free type of $a$ in $M$, meaning the set of all quantifier-free formulas true of $a$. If the theory \begin{align*} T \cup p_{\mathrm{qf}}(a) \cup \{\neg \varphi(x_1,\dots,x_n)\} \end{align*} had a model, then there would be $N \models T$ and $b \in N^n$ such that $b$ satisfies every quantifier-free formula true of $a$, while $N \models \neg\varphi(b)$. Since $p_{\mathrm{qf}}(a)$ is complete for quantifier-free formulas, this means $a$ and $b$ have the same quantifier-free type. The previous step then forces \begin{align*} M \models \varphi(a) \quad \Longleftrightarrow \quad N \models \varphi(b), \end{align*} contradicting $N \models \neg\varphi(b)$. Therefore the displayed theory is inconsistent. By the compactness theorem for first-order logic, already a finite part of $p_{\mathrm{qf}}(a)$ is enough to force $\varphi$ over $T$. Hence there are quantifier-free formulas $\eta_1,\dots,\eta_m$ true of $a$ such that \begin{align*} T \models \forall x_1\cdots\forall x_n\,\bigl((\eta_1 \wedge \cdots \wedge \eta_m) \to \varphi\bigr). \end{align*} The conjunction \begin{align*} \theta_a := \eta_1 \wedge \cdots \wedge \eta_m \end{align*} is quantifier-free, belongs to $\mathcal Q_\varphi$, and is true of $a$. Now we need one formula, not a different formula $\theta_a$ for each realization $a$. Suppose no finite disjunction of formulas from $\mathcal Q_\varphi$ covers all realizations of $\varphi$. Equivalently, the set \begin{align*} T \cup \{\varphi(x_1,\dots,x_n)\} \cup \{\neg\theta(x_1,\dots,x_n) : \theta \in \mathcal Q_\varphi\} \end{align*} would be satisfiable. A realization $a$ of this set would satisfy $\varphi$ while avoiding every quantifier-free formula that implies $\varphi$, contradicting the paragraph above. Therefore the set is inconsistent, and compactness gives finitely many formulas $\theta_1,\dots,\theta_r \in \mathcal Q_\varphi$ such that \begin{align*} T \models \forall x_1\cdots\forall x_n\,\bigl(\varphi \to (\theta_1 \vee \cdots \vee \theta_r)\bigr). \end{align*} Because each $\theta_i$ belongs to $\mathcal Q_\varphi$, the reverse implication also holds: \begin{align*} T \models \forall x_1\cdots\forall x_n\,\bigl((\theta_1 \vee \cdots \vee \theta_r) \to \varphi\bigr). \end{align*} Thus \begin{align*} \psi := \theta_1 \vee \cdots \vee \theta_r \end{align*} is a quantifier-free formula equivalent to $\varphi$ modulo $T$.[/guided]