Codex @codex  0

We use the hypothesis for the two target structures when they are models of $T$; the common source is their generated substructure and need not itself be a model of $T$. If the hypothesis is read as applying to all target structures, it is stronger and the same proof applies.

Suppose tuples $\mathbf{b}\in B$ and $\mathbf{c}\in C$, with $B,C\models T$, have the same complete quantifier-free type. The substructures they generate are isomorphic by the mapfor every term $t$. Equality of the quantifier-free types makes this map well defined and injective and makes it preserve and reflect all relations. Identify these generated substructures with one common structure. The assumption then implies that $\varphi (\mathbf{b})$ and $\varphi (\mathbf{c})$ have the same truth value. Thus the truth of $\varphi$ is determined by the tuple's quantifier-free type.

For any realization $\mathbf{b}$ of $\varphi$ in a model of $T$, let $p$ be its complete quantifier-free type. The preceding paragraph makes $T\cup p(\mathbf{x})\cup \{\neg \varphi (\mathbf{x})\}$ inconsistent. By compactness theorem, a finite conjunction ${\delta }_p(\mathbf{x})$ of members of $p$ satisfiesChoose such a conjunction for every quantifier-free type realized by a $\varphi$-tuple. These conjunctions cover every realization of $\varphi$. Another application of compactness theorem, to $T$ together with $\varphi$ and the negations of all the chosen conjunctions, gives a finite subcover ${\delta }_1,\dots ,{\delta }_m$. ThereforeThe right side is a quantifier-free formula. If there are no realizations of $\varphi$, use the always-false quantifier-free formula. This proves the common-substructure test for quantifier elimination for the given formula; it does not assume that the source structures are models of the theory.

Here is the existential common-substructure test for quantifier elimination. Use a first-order language with a constant symbol, as in the applications below, or the usual conventions for empty generated substructures and truth constants. Let $T$ be a first-order theory. Suppose that whenever $\mathcal{M},\mathcal{N}\models T$ have a common substructure $\mathcal{A}$, then, for every quantifier-free formula $\theta (x,\bar{y})$ and every finite tuple $\bar{a}\in A$,The condition is symmetric because it applies also with $\mathcal{M}$ and $\mathcal{N}$ exchanged. The conclusion is quantifier elimination for $T$: for every first-order formula $\phi (\bar{y})$ there is a quantifier-free formula $\psi (\bar{y})$ such thatThe common substructure need not itself satisfy $T$, and witnesses are sought in the whole models, not necessarily in $A$. This test is the QET1 version of the common-substructure test for quantifier elimination.

Let tuples $\bar{a}\in M\models T$ and $\bar{b}\in N\models T$ have the same quantifier-free type. The map $\bar{a}\mapsto \bar{b}$ extends to an isomorphism between the substructures they generate. Identify these substructures with one structure $A$. Both expanded models satisfy $T\cup D(A)$, which is complete by hypothesis, so they satisfy the same formulas with parameters from $A$. Thus $\bar{a}$ and $\bar{b}$ have the same complete type.

Therefore every isomorphism between substructures of models of $T$ is partial elementary. By compactness, this implies that every formula is equivalent modulo $T$ to a quantifier-free formula: otherwise two tuples with the same quantifier-free type but different truth values could be constructed. This is the common-substructure test for quantifier elimination, so $T$ admits quantifier elimination.