A theory *T* is **model complete** if it satisfies one of the following equivalent conditions:

- Whenever
*M*⊆*N*is an inclusion of models of*T*,*M*is an elementary substructure of*N*. - Every model of
*T*is existentially closed. - Every formula is equivalent, mod
*T*, to a universal formula. - Every formula is equivalent, mod
*T*, to an existential formula. - Every universal formula is equivalent, mod
*T*, to an existential formula. - Every existential formula is equivalent, mod
*T*, to a universal formula.

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 *y*_{i}'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. ::: ::: :::