= Solution
It suffices to eliminate one <existential quantifier> from a <quantifier-free formula> $\theta(y,\bar x)$. Indeed, <logical connectives> preserve equivalence, and a <universal quantifier> can be rewritten using $\forall y\,\alpha\equiv\neg\exists y\,\neg\alpha$. An induction on the construction of a <first-order formula> then eliminates all its <quantifiers> from the inside out.
Convert $\theta$ to <disjunctive normal form>. Since <existential quantification> distributes over a finite <logical disjunction>, consider a single <logical conjunction> of atomic <first-order formulas> and their negations. There are no function or constant symbols in this <first-order signature>, so its atoms are equalities between variables and instances of $E$ between variables.
For a tuple $\bar x=(x_1,\ldots,x_r)$, enumerate its possible complete atomic diagrams $\delta(\bar x)$. Such a <quantifier-free formula> specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which <first-order equality> is an <equivalence relation> and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a <first-order model> of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one <vertex> for each equality class successively, using the extension axioms to prescribe its adjacency to earlier <vertices>.
Fix one diagram $\delta$. A potential <existential witness> for $y$ has one of two forms.
* \b[An existing <vertex>.] If $y=x_i$, substitute $x_i$ for $y$ in the <logical conjunction>. The diagram $\delta$ decides the <truth value> of every resulting atom, and so decides whether this choice works.
* \b[A new <vertex>.] Require $y\ne x_i$ for every $i$. Simplify $y=y$ to true and $E(y,y)$ to false. Use symmetry to rewrite every remaining edge requirement involving $y$ in the form $E(x_i,y)$ or $\neg E(x_i,y)$. An equality $y=x_i$, a positive loop requirement, or opposite edge requirements on the same equality class makes this case impossible. Otherwise the requirements give a consistent adjacency pattern on finitely many distinct <vertices>. Any equality classes without a specified edge requirement can be assigned either pattern. Reorder representatives with the desired neighbours first; the appropriate extension axiom supplies a fresh <vertex> with precisely this pattern.
All <first-order formulas> involving only $\bar x$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal D$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. Then
$$
\boxed{T\models\forall\bar x\left[
\exists y\,\theta(y,\bar x)\leftrightarrow
\bigvee_{\delta\in\mathcal D}\delta(\bar x)\right].}
$$
The right side is a <quantifier-free formula>. An empty <logical disjunction> means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed <first-order sentences> in this constant-free <first-order signature>.
For a concrete illustration of the fresh-witness case,
$$
T\models\forall x_1\forall x_2\forall x_3\left[
\exists y\,(E(y,x_1)\land\neg E(y,x_2)\land y\ne x_3)
\leftrightarrow x_1\ne x_2\right].
$$
If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a <vertex> outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves <quantifier elimination>.
Back to article page
