nLab substructure complete theory




One wants an equivalent and purely semantic characterization of quantifier elimination.

A theory TT is substructure complete if after fixing a substructure, the theory of the elementary class of all TT-models into which that substructure embeds is complete.



A first-order theory TT in a language \mathcal{L} is substructure complete if for any MMod(T)M \in \mathbf{Mod}(T) and any \mathcal{L}-substructure AM,A \hookrightarrow M, the theory T Diag(A)T_{\mathsf{Diag}(A)} (expansion by AA‘s quantifier-free diagram)—whose models are precisely those models NMod(T)N \in \mathbf{Mod}(T) such that there exists an embedding of \mathcal{L}-structures ANA \hookrightarrow N—is complete.

Equivalence with quantifier elimination


TT eliminates quantifiers if and only if TT is substructure-complete.


()(\Rightarrow) Suppose TT eliminates quantifiers. Fix a substructure AA. 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,NMod(T)M, N \in \mathbf{Mod}(T)

MAN M \leftarrow A \rightarrow N

containing AA, we have that for every sentence φ\varphi satisfied by NN, TφψT \models \varphi \leftrightarrow \psi where ψ\psi is quantifier-free. Therefore, ψ\psi transfers to AA and MM, so MφM \models \varphi as well, and vice-versa.

()(\Leftarrow) Now suppose TT is substructure complete. Fix φ(x)\varphi(x) an \mathcal{L}-formula. Consider the type Φ\Phi of its quantifier-free consequences,i .e.

Φ(x)=df{φ *(x) quantifier-free |Tφφ *}. \Phi(x) \overset{\operatorname{df}}{=} \{\varphi^*(x) \text{ quantifier-free } \operatorname{|} T \models \varphi \implies \varphi^*\}.

(This thing is like the quantifier-free principal ultrafilter on φ\varphi in the Boolean algebra of definable sets.)

Let d 1,,d nd_1, \dots, d_n be distinct new constant symbols. Write d=d=(d 1,,d n)d = \vec{d} = (d_1, \dots, d_n).

Claim: TΦ(d)φ(d).T \cup \Phi(d) \models \varphi(d).

(This claim says, roughly, that knowing the principal ultrafilter of quantifier-free definable sets containing φ(x)\varphi(x) suffices to pin down φ(x)\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 ATΦ(d){¬φ(d)}.A \models T \cup \Phi(d) \cup \{\not \varphi(d)\}. (This is a structure in the language \mathcal{L} of TT, expanded by dd.) Let d Ad^A be the interpretation of the new constants dd in AA. Consider the finitely-generated \mathcal{L}-substructure of AA around d Ad^A:

C=dfd A . C \overset{\operatorname{df}}{=} \langle d^A \rangle_{\mathcal{L}}.

Subclaim: T{φ(d A)}Diag(C)T \cup \{\varphi(d^A)\} \cup \mathsf{Diag}(C) is satisfiable.

(This subclaim amounts to saying that while AA models ¬φ(d A)\neg \varphi(d^A), we can find another model BTB \models T, embedding CC, such that BB does models φ(d A)\varphi(d^A).)

Proof of subclaim: this will be a standard compactness argument. Suppose not; by compactness there exist finitely many sentences θ 1,,θ mDiag(C)\theta_1, \dots, \theta_m \in \mathsf{Diag}(C) such that

T{φ(d A)}{θ i} 1im T \cup \{\varphi(d^A)\} \cup \{\theta_i\}_{1 \leq i \leq m}

is not satisfiable. By the definition of quantifier-free diagram, we can write θ i=θ i(d A)\theta_i = \theta'_i(d^A), where θ i\theta'_i is a quantifier-free \mathcal{L}-formula.


T{φ(d A),θ 0(d A),θ 1(d A),,θ m(d A)} T \cup \{\varphi(d^A), \theta'_0(d^A), \theta'_1(d^A), \dots, \theta_m'(d^A)\}

is not satisfiable, where (remembering that d Ad^A is now just a tuple of constant symbols) θ 0(x)\theta'_0(x) specifies that all the entries of xx are distinct.


Tφ(d A) i=0 m¬θ i(d A). T \models \varphi(d^A) \rightarrow \bigvee_{i = 0}^m \neg \theta'_i(d^A).

Since there are no constraints on the constant symbols d Ad^A and θ 0\theta'_0 specifies that they are all distinct, we may generalize them, so that

Tx(φ(x) i=0 m¬θ i(x)) T \models \forall x \left( \varphi(x) \to \bigvee_{i = 0}^m \neg \theta'_i(x) \right)


i=0 m¬θ i(x)Φ(x). \bigvee_{i = 0}^m \neg \theta'_i(x) \in \Phi(x).

Now, by assumption, AΦ(d)A \models \Phi(d). This means in particular that A i=0 m¬θ i(d A).A \models \bigvee_{i = 0}^m \neg \theta'_i(d^A).

Since that disjunction is quantifier-free, it transfers down to CC. Therefore, there is some 0jm0 \leq j \leq m such that C¬θ j(d A).C \models \neg \theta'_j(d^A). Since the d Ad^A were distinct when we obtained AA (from which we obtained CC), we can rule out j0j \neq 0. But for each j=1,,mj = 1, \dots, m, θ j=θ j(d A)Diag(C)\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 BT{φ(d A)}Diag(C).\mathbf{B} \models T \cup \{\varphi(d^A)\} \cup \mathsf{Diag}(C).


A¬φ(d A), and Bφ(d A), A \models \neg \varphi(d^A), \text{ and } B \models \varphi(d^A),

which contradicts substructure completeness over CC.

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Φ(x)φ(d)T \cup \Phi(x) \models \varphi(d) is finitely supported, so that there are finitely many φ 1 *,,φ m *Φ(x)\varphi^*_1, \dots, \varphi^*_m \in \Phi(x) such that

T{φ i *(d)} imφ(d). T \cup \{\varphi_i^*(d)\}_{i \leq m} \models \varphi(d).

Write φ *=df imφ i *.\varphi^* \overset{\operatorname{df}}{=} \bigvee_{i \leq m} \varphi_i^*. Again, we generalize the constants dd, obtaining

Tx(φφ *). T \models \forall x \left( \varphi \leftrightarrows \varphi^* \right).

Since the φ i *\varphi^*_i are all quantifier-free, and φ\varphi was arbitrary, we have proved that TT eliminates quantifiers.



  • The analogous (and weaker) property where one asks that the theory of the elementary class of TT-models embedding a fixed TT-model is complete is called model completeness.

  • Of course, substructure-completeness implies model-completeness.


  • Dave Marker, Model theory: an introduction, theorem 3.14

Last revised on June 11, 2022 at 10:50:15. See the history of this page for a list of all contributions to it.