General resolution in first order logic

Question

Assuming you have a formula in first order logic like

$$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$ (which seems valid?)

Converting the formula to CNF:

$$(\neg p(x) \vee \neg q(y) \vee p(z)) \land (\neg p(x) \vee \neg q(y) \vee q(z)) $$

I don't see how I can apply general resolution to get the empty clause in this case which puzzles me since I believe the formula is valid.

Answer 1

As you correctly point out, the original formula is valid (in every model either there is some element for which p or q doesn't hold, or p and q hold for all elements).

To prove that your formula is valid, you cannot use resolution directly. Recall that with resolution, you can derive the empty clause from a clause set iff the clause set is unsatisfiable. Your formula is valid iff its negation is unsatisfiable. So to prove your formula is valid, you have to derive the empty clause from the clause set corresponding to the negation of your formula.

Let $\varphi$ be your original formula. $$\lnot \varphi \equiv \forall_x \forall_y \exists_z (px \land qy \land (\lnot pz \lor \lnot qz))$$ Skolemization replaces $z$ by a function symbol $f(x,y)$: $$\lnot \varphi \equiv_{SAT} \forall_x \forall_y (px \land qy \land (\lnot pfxy \lor \lnot qfxy))$$ The corresponding clause set: $$\{\{px\},\{qy\},\{\lnot pfxy, \lnot qfxy\}\}$$ From there it should be straight-forward to derive the empty clause:

• Apply renaming $\nu_1 = \{x/x_1\}$ to $\{px\}$, yielding $\{px_1\}$, then resolve $\{p x_1 \}$ with $\{ \lnot pfxy, \lnot qfxy\}$ by $\sigma_1 = \{ x_1 / fxy\}$, yielding $\{\lnot q fxy\}$
• Apply renaming $\nu_2 = \{y / y_1\}$ to $\{qy\}$, yielding $\{qy_1\}$, then resolve $\{qy_1\}$ with $\{ \lnot qfxy \}$ by $\sigma_2 = \{y_1/fxy\}$, yielding the empty clause $\Box$

In conclusion, we have shown by resolution that $\lnot \varphi$ is unsatisfiable. Therefore $\varphi$ is valid.