Applying resolution to Predicate Calculus

Question

Prove the conclusion (∀x) Q(x) via resolution given the premises:

(∀x){P(x)->Q(x)} and ¬(∃x){¬Q(x)}

Do I just negate the conclusion and start knocking out clauses that contradict each other? Example clauses could be Q(x) and ¬Q(x)?

Answer 1

First, you need to get your clauses, and to do that, you need to get the statements into Prenex Normal Form (i.e. Get the quntifiers to the front of the statements), get their bodies into CNF, and skolemize if needed.

Ok, the first premise:

$\forall x (P(x) \rightarrow Q(x))$

Becomes:

$\forall x (\neg P(x) \lor Q(x))$

And now we drop the universal quantifier, giving us the first clause:

$\{ \neg P(x), Q(x) \}$

The second premise:

$\neg \exists x \neg Q(x)$

Apply quantifier negation to get:

$\forall x \neg \neg Q(x)$

double negation:

$\forall x Q(x)$

Change variable (we already use variable $x$ in the first clause), and drop quantifier' and we have our second clause:

$\{ Q(y) \}$

Negate the conclusion:

$\neg \forall x Q(x)$

Quantifier negation:

$\exists x \neg Q(x)$

skolemize, and we have our third clause:

$\{ \neg Q(a) \}$

OK, now resolve. Well, resolve clauses two and three by substituting $a$ for $y$, and you get ... the empty clause!

We have reached a contradiction (the empty clause represents a contradiction), so this tells us that apparently the conclusion cannot be false if the premises are true. And that means the conclusion does indeed validly follow from the premises. (And you'll notice that in fact the conclusion follows from the second premise alone, since the second and third clause lead immediately to the contradiction ... In fact while we were rewriting the second premise to get it into the right form for resolution, it already became the conclusion!)

ADDENDUM

@FabioSomenzi pointed out that the proof would be more interesting if the second premise were $\neg \exists x \neg P(x)$ (indeed, I agree with him that it probably is and that there is a typo). So, let's work with that. Now, the clauses you end up getting with that change are:

1. $\{ \neg P(x), Q(x) \}$

2. $\{ P(y) \}$

3. $\{ \neg Q(a) \}$

Resolve:

4. $\{ \neg P(a) \}$ 1,3, a/x

5. $\{ \}$ 2,4, a/y