Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 2 / d / 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,\dots ,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.

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. ThenThe 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,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.