§ Why FOL models must be nonempty

• We ask for nonemptiness to ensure rules like (forall x. x = x) is equialent to exists x. x != x.