indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
One wants an equivalent and purely semantic characterization of quantifier elimination.
A theory is substructure complete if after fixing a substructure, the theory of the elementary class of all -models into which that substructure embeds is complete.
A first-order theory in a language is substructure complete if for any and any -substructure the theory (expansion by ‘s quantifier-free diagram)—whose models are precisely those models such that there exists an embedding of -structures —is complete.
eliminates quantifiers if and only if is substructure-complete.
Suppose eliminates quantifiers. Fix a substructure . 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
containing , we have that for every sentence satisfied by , where is quantifier-free. Therefore, transfers to and , so as well, and vice-versa.
Now suppose is substructure complete. Fix an -formula. Consider the type of its quantifier-free consequences,i .e.
(This thing is like the quantifier-free principal ultrafilter on in the Boolean algebra of definable sets.)
Let be distinct new constant symbols. Write .
Claim:
(This claim says, roughly, that knowing the principal ultrafilter of quantifier-free definable sets containing suffices to pin down . 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 (This is a structure in the language of , expanded by .) Let be the interpretation of the new constants in . Consider the finitely-generated -substructure of around :
Subclaim: is satisfiable.
(This subclaim amounts to saying that while models , we can find another model , embedding , such that does models .)
Proof of subclaim: this will be a standard compactness argument. Suppose not; by compactness there exist finitely many sentences such that
is not satisfiable. By the definition of quantifier-free diagram, we can write , where is a quantifier-free -formula.
Therefore,
is not satisfiable, where (remembering that is now just a tuple of constant symbols) specifies that all the entries of are distinct.
Therefore,
Since there are no constraints on the constant symbols and specifies that they are all distinct, we may generalize them, so that
hence
Now, by assumption, . This means in particular that
Since that disjunction is quantifier-free, it transfers down to . Therefore, there is some such that Since the were distinct when we obtained (from which we obtained ), we can rule out . But for each , . This is a contradiction.
This proves the subclaim.
Now we proceed with proving the claim.
Let
Then:
which contradicts substructure completeness over .
This proves the claim.
Now we proceed with proving the theorem.
With the claim in hand, the compactness theorem tells us that the entailment is finitely supported, so that there are finitely many such that
Write Again, we generalize the constants , obtaining
Since the are all quantifier-free, and was arbitrary, we have proved that 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 -models embedding a fixed -model is complete is called model completeness.
Of course, substructure-completeness implies model-completeness.
Last revised on June 11, 2022 at 10:50:15. See the history of this page for a list of all contributions to it.