Deciding Exists-Forall Class

Theorem: Consider formula $G$ of the form $\forall x_1,\ldots,x_n.F$ where $F$ is quantifier free formula of first-order logic with equality, without function symbols (only constants and relation symbols). Then there exists a structure in which the formula is true iff the formula is true in some structure whose domain is the set of constants in $F$ .

Proof: Suppose that $\alpha$ is a model for $G$ . Let $c_1,\ldots,c_n$ . Pick a substructure of this model obtained by throwing away all elements other than the interpretation of constants $c_1,\ldots,c_n$ . We claim that we obtain a model for $G$ and keeping the definition of relations and predicates on $c_1,\ldots,c_n$ as in the structure. If we pick arbitrary values of $x_1,\ldots,x_n$ from the set $\{c_1,\ldots,c_n\}$ , then $F$ evaluates to true because it evaluated to true in the original structure. Therefore, $F$ holds in the model for such structure. End of proof.

Note: there exists a counterpart of this theorem for function symbols, which ensures the existence of countable models for arbitrary first-order logic formulas. This is the Herbrand's theorem.

Example:

Consider the following formula:

$\begin{equation*} \begin{array}{l} (\forall x,y,z.\ r(x,y) \land r(x,z) \rightarrow y=z) \land \\ (\forall x,y,z.\ r(x,z) \land r(y,z) \rightarrow x=y) \land \\ (\forall x,y.\ P(x) \land r(x,y) \rightarrow Q(y)) \\ P(a) \land P(b) \land Q(c) \land \lnot P(c) \end{array} \end{equation*}$

The formula is true iff the following formula over the domain $D = \{a,b,c\}$ is true:

$\begin{equation*} \begin{array}{l} \displaystyle \big(\bigwedge_{x,y,z \in \{a,b,c\}}.\ r(x,y) \land r(x,z) \rightarrow y=z\big) \land \\ \displaystyle \big(\bigwedge_{x,y,z \in \{a,b,c\}}.\ r(x,z) \land r(y,z) \rightarrow x=y\big) \land \\ \displaystyle \big(\bigwedge_{x,y \in \{a,b,c\}}.\ P(x) \land r(x,y) \rightarrow Q(y)\big) \land \\ P(a) \land P(b) \land Q(c) \land \lnot P(c) \end{array} \end{equation*}$

It suffices to search for the possible definitions of $r,P,Q$ in domains of size 3 or less (it could happen that some of $a,b,c$ are equal).

Thus we can find a model for the original formula.

Example: Prove that the following formula is valid:

$\begin{equation*} L \subseteq A \land L \subseteq B \rightarrow L \subseteq A \cap B \end{equation*}$

We check for counterexamples:

$\begin{equation*} L \subseteq A \land L \subseteq B \land \lnot (L \subseteq A \cap B) \end{equation*}$

We express set operations using quantifiers:

$\begin{equation*} (\forall x. L(x) \rightarrow A(x)) \land (\forall y. L(y) \subseteq B(y)) \land \lnot (\forall z. L(z) \rightarrow A(z) \land B(z))) \end{equation*}$

We propagate the negation:

$\begin{equation*} (\forall x. L(x) \rightarrow A(x)) \land (\forall y. L(y) \subseteq B(y)) \land \exists z. (L(z) \land \lnot (A(z) \land B(z))) \end{equation*}$

We replace the existential quantifier at the top level with a fresh constant $c$ :

$\begin{equation*} (\forall x. L(x) \rightarrow A(x)) \land (\forall y. L(y) \subseteq B(y)) \land (L(c) \land \lnot (A(c) \land B(c))) \end{equation*}$

Now it follows that it suffices to check the formula on the domain $D = \{c\}$ . The formula reduces to:

$\begin{equation*} (L(c) \rightarrow A(c)) \land (L(c) \subseteq B(c)) \land (L(c) \land \lnot (A(c) \land B(c))) \end{equation*}$

If we treat $L(c),A(c),B(c)$ as propositional variables, we conclude that the formula is unsatisfiable. Therefore, the original formula is unsatisfiable.