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
∃z : y − x = z2
and a universal definition
∀z, w : w(x − y) ≠ 1 ∨ z2 ≠ (x − y)
Another notable model complete theory, without quantifier elimination, is ACFA.
Conditions (3) and (4) are equivalent by De Morgan's Laws: ϕ(x) is equivalent to a universal formula if and only if ¬ϕ(x) 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
∀y1∃y2∀y3⋯Qyn : ϕ(x, y1, …, yn)
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
¬∃y2∀y3⋯Qyn : ϕ ≡ ∀y2∃y3⋯¬ϕ,
must be equivalent to a universal formula. Consequently,
∃y2∀y3⋯Qyn : ϕ
is equivalent to an existential formula. By condition (6), it is equivalent to some universal formula
∀z : ψ(x; y1; z)
Then the original formula is equivalent to
∀y1∀z : ψ(x; y1; z)
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 ϕ(x) and every tuple a from M, we have
M ⊨ ϕ(a) ⇔ N ⊨ ϕ(a)
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 ϕ(x) is a formula and c is a tuple from M, then
M ⊨ ϕ(a) ⇒ N ⊨ ϕ(a)
But this is one of the characterizations of universal formulas, so ϕ(x) 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 ϕ(x) be a formula, and c be a tuple from M. We need to show that
M ⊨ ϕ(c) ⇔ N ⊨ ϕ(c) ( * )
By (3) and (4), we can find existential and universal formulas ψ(x) and χ(x), respectively, which are equivalent mod T to ϕ(x).
Now universal formulas are always preserved downwards, and existential formulas are preserved upwards, so
M ⊨ ψ(c) ⇒ N ⊨ ψ(c)
N ⊨ χ(c) ⇒ M ⊨ χ(c)
As ϕ(x), ψ(x), and χ(x) are all equivalent, we obtain the desired (*) above.
QED. ::: ::: :::