[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$.
[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]
[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*}
[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]
[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.
[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]
[/step]
