indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
One wants an equivalent and purely semantic characterization of quantifier elimination.
A theory $T$ is substructure complete if after fixing a substructure, the theory of the elementary class of all $T$-models into which that substructure embeds is complete.
A first-order theory $T$ in a language $\mathcal{L}$ is substructure complete if for any $M \in \mathbf{Mod}(T)$ and any $\mathcal{L}$-substructure $A \hookrightarrow M,$ the theory $T_{\mathsf{Diag}(A)}$ (expansion by $A$‘s quantifier-free diagram)—whose models are precisely those models $N \in \mathbf{Mod}(T)$ such that there exists an embedding of $\mathcal{L}$-structures $A \hookrightarrow N$—is complete.
$T$ eliminates quantifiers if and only if $T$ is substructure-complete.
$(\Rightarrow)$ Suppose $T$ eliminates quantifiers. Fix a substructure $A$. Since quantifier-free sentences are automatically transferred by embeddings (whereas without the additional property of quantifier-freeness, we would require the additional property that an embedding be elementary), then for any two models $M, N \in \mathbf{Mod}(T)$
containing $A$, we have that for every sentence $\varphi$ satisfied by $N$, $T \models \varphi \leftrightarrow \psi$ where $\psi$ is quantifier-free. Therefore, $\psi$ transfers to $A$ and $M$, so $M \models \varphi$ as well, and vice-versa.
$(\Leftarrow)$ Now suppose $T$ is substructure complete. Fix $\varphi(x)$ an $\mathcal{L}$-formula. Consider the type $\Phi$ of its quantifier-free consequences,i .e.
(This thing is like the quantifier-free principal ultrafilter on $\varphi$ in the Boolean algebra of definable sets.)
Let $d_1, \dots, d_n$ be distinct new constant symbols. Write $d = \vec{d} = (d_1, \dots, d_n)$.
Claim: $T \cup \Phi(d) \models \varphi(d).$
(This claim says, roughly, that knowing the principal ultrafilter of quantifier-free definable sets containing $\varphi(x)$ suffices to pin down $\varphi(x)$. After establishing the claim, it will be easy to improve it to full quantifier elimination.)
Proof of claim: suppose towards a contradiction that there exists an $A \models T \cup \Phi(d) \cup \{\not \varphi(d)\}.$ (This is a structure in the language $\mathcal{L}$ of $T$, expanded by $d$.) Let $d^A$ be the interpretation of the new constants $d$ in $A$. Consider the finitely-generated $\mathcal{L}$-substructure of $A$ around $d^A$:
Subclaim: $T \cup \{\varphi(d^A)\} \cup \mathsf{Diag}(C)$ is satisfiable.
(This subclaim amounts to saying that while $A$ models $\neg \varphi(d^A)$, we can find another model $B \models T$, embedding $C$, such that $B$ does models $\varphi(d^A)$.)
Proof of subclaim: this will be a standard compactness argument. Suppose not; by compactness there exist finitely many sentences $\theta_1, \dots, \theta_m \in \mathsf{Diag}(C)$ such that
is not satisfiable. By the definition of quantifier-free diagram, we can write $\theta_i = \theta'_i(d^A)$, where $\theta'_i$ is a quantifier-free $\mathcal{L}$-formula.
Therefore,
is not satisfiable, where (remembering that $d^A$ is now just a tuple of constant symbols) $\theta'_0(x)$ specifies that all the entries of $x$ are distinct.
Therefore,
Since there are no constraints on the constant symbols $d^A$ and $\theta'_0$ specifies that they are all distinct, we may generalize them, so that
hence
Now, by assumption, $A \models \Phi(d)$. This means in particular that $A \models \bigvee_{i = 0}^m \neg \theta'_i(d^A).$
Since that disjunction is quantifier-free, it transfers down to $C$. Therefore, there is some $0 \leq j \leq m$ such that $C \models \neg \theta'_j(d^A).$ Since the $d^A$ were distinct when we obtained $A$ (from which we obtained $C$), we can rule out $j \neq 0$. But for each $j = 1, \dots, m$, $\theta_j = \theta'_j(d^A) \in \mathsf{Diag}(C)$. This is a contradiction.
This proves the subclaim.
Now we proceed with proving the claim.
Let $\mathbf{B} \models T \cup \{\varphi(d^A)\} \cup \mathsf{Diag}(C).$
Then:
which contradicts substructure completeness over $C$.
This proves the claim.
Now we proceed with proving the theorem.
With the claim in hand, the compactness theorem tells us that the entailment $T \cup \Phi(x) \models \varphi(d)$ is finitely supported, so that there are finitely many $\varphi^*_1, \dots, \varphi^*_m \in \Phi(x)$ such that
Write $\varphi^* \overset{\operatorname{df}}{=} \bigvee_{i \leq m} \varphi_i^*.$ Again, we generalize the constants $d$, obtaining
Since the $\varphi^*_i$ are all quantifier-free, and $\varphi$ was arbitrary, we have proved that $T$ eliminates quantifiers.
By the above theorem, any theory which eliminates quantifiers is substructure complete.
So e.g. the countable random graph, the theory ACF of algebraically closed fields, the theory DLO of dense linear orders…
The analogous (and weaker) property where one asks that the theory of the elementary class of $T$-models embedding a fixed $T$-model is complete is called model completeness.
Of course, substructure-completeness implies model-completeness.