Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 23 / 2

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.

In the language of a single edge relation $E$, axiomatize an undirected loop-free graph byFor every pair of nonnegative integers $r,s$, add the extension axiom demanding, for any distinct $u_1,\dots ,u_r,v_1,\dots ,v_s$, a new vertex $z$ such thatThese axioms form the theory of the random graph. Repetition of the fresh-vertex requirement also forces infinitude.

To prove quantifier elimination, first eliminate one existential quantifier from a quantifier-free formula. Put that formula into disjunctive normal form, so it suffices to consider a conjunction of literals in a new variable $z$ and the parameter variables. There are two possibilities for a witness: $z$ equals one of the parameters, in which case substitution gives a quantifier-free condition; or $z$ is distinct from all of them. In the latter case, the graph axioms reduce all requirements involving $z$ to specified adjacency or nonadjacency to the distinct parameter vertices. A requirement $E(z,z)$ is impossible, and conflicting requirements at equal parameter vertices are impossible. Every other consistent adjacency pattern is realized by the extension axiom.

There are only finitely many equality patterns of the given parameter tuple. For each, consistency of the literals is a quantifier-free condition, including the unchanged relations among the parameters. Their finite disjunction describes exactly when a witness exists. Thus $\exists z\theta (z,\mathbf{x})$ is equivalent to a quantifier-free formula whenever $\theta$ is quantifier-free. Mathematical induction on formulas now eliminates all quantifiers, using $\forall z\theta \equiv \neg \exists z\neg \theta$. Hence the random-graph theory eliminates quantifiers. The extension axioms also yield the usual countable random graph by a back-and-forth construction.