A theory T is model complete if it satisfies one of the following equivalent conditions:
See below for a proof that these notions are equivalent.
Theories with quantifier elimination are model complete. This includes ACF, RCF (in the language with ≤), DLO, and ACVF. Even in the pure field language, RCF is model complete, because x ≤ y admits an existential definition
and a universal definition
Another notable model complete theory, without quantifier elimination, is ACFA.
Conditions (3) and (4) are equivalent by De Morgan's Laws: is equivalent to a universal formula if and only if is equivalent to an existential formula. Conditions (5) and (6) are similarly equivalent.
Conditions (3-4) clearly imply (5-6). Conversely, assume (5-6). We show by induction on n that any formula of the form
is equivalent to a universal formula, where the yi's are tuples, Q is the appropriate quantifier, and is quantifier-free. The base case where n = 1 is trivial.
For n > 1, the inductive hypothesis implies that
,
must be equivalent to a universal formula. Consequently,
is equivalent to an existential formula. By condition (6), it is equivalent to some universal formula
Then the original formula is equivalent to
which is a universal formula. This completes the inductive proof that any formula in prenex form is equivalent to a universal formula. Any formula can be put in prenex form, so condition (3) holds.
So conditions (3-6) are all equivalent.
It remains to show that (1) implies (2) implies (3-6) implies (1).
Suppose (1) holds, and let us prove (2). We need to prove that whenever M ⊆ N is an inclusion of models of T, then M is existentially closed in M. This means that for every existential formula and every tuple a from M, we have
Obviously this is a weaker condition than M being an elementary substructure of N, so (1) certainly implies (2).
Now assume (2). Then whenever M ⊆ N is an inclusion of models of T, M is existentially closed in T. So if is a formula and c is a tuple from M, then
But this is one of the characterizations of universal formulas, so must be equivalent (mod T) to a universal formula. Therefore (6) holds.
Finally, assume (3-6). Let M ⊆ N be an inclusion of models. We need to show that M is an elementary substructure of N. Let be a formula, and c be a tuple from M. We need to show that
By (3) and (4), we can find existential and universal formulas and , respectively, which are equivalent mod T to .
Now universal formulas are always preserved downwards, and existential formulas are preserved upwards, so
As , , and are all equivalent, we obtain the desired (*) above.
QED. ::: ::: :::