= Solution
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$,
$$
\mathcal M\models\exists x\,\theta(x,\bar a)
\quad\Longrightarrow\quad
\mathcal N\models\exists x\,\theta(x,\bar a).
$$
The condition is symmetric because it applies also with $\mathcal M$ and $\mathcal N$ exchanged. The conclusion is \b[<quantifier elimination> for $T$]: for every <first-order formula> $\varphi(\bar y)$ there is a <quantifier-free formula> $\psi(\bar y)$ such that
$$
T\models\forall\bar y\bigl(\varphi(\bar y)\leftrightarrow\psi(\bar y)\bigr).
$$
The 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>.
Back to article page
