So, I have to prove the validity of the following formula:
F = ∃x[(P(x) → P(a)) ∧ (P(x) → P(b))]
To do this, using resolution, should I negate my F and then if I can get a resolvent that is the empty set this will prove that the negation of F is unsatisfiable meaning that F is valid?
Update:
Negate F:
¬∃x[(P(x) → P(a)) ∧ (P(x) → P(b))]
∀x¬[(P(x) → P(a)) ∧ (P(x) → P(b))]
Get rid of implications:
∀x¬[(¬P(x) ∨ P(a)) ∧ (¬P(x) ∨ P(b))]
Import negation:
∀x[(P(x) ∧ ¬P(a)) ∨ (P(x) ∧ ¬P(b))]
Distribute:
∀x[(P(x) ∨ ¬P(a)) ∧ (¬P(b) ∨ ¬P(a)) ∧ (P(x) ∨ P(x)) ∧(P(x) ∨ ¬P(b))]
Clauses:
1) {P(x), ¬P(a)}
2) {¬P(b), ¬P(a)}
3) {P(x)}
4) {P(x), ¬P(b)}
Resolution:
5) Resolvent of clause 1 & 2, [x/b]: {¬P(a)}
6) Resolvent of clause 3 & 5, [x/a]: {}
¬F is unsatisfiable, therefore F is valid.