My question is very simple: how can I prove that binary resolution is not complete in First-Order Logic? I have found a first attempt of explaination by means of counterexample in which I have:
$\forall x \forall y (P(x) \lor P(y))$
$\exists u \exists v (P(u) \wedge P(v))$.
The example tries to show that 1 follows from 2 . It brings both sentences in CNF (so far so good) therefore they became:
$(P(x) \lor P(y))$
$(\lnot P(u) \lor \lnot P(v))$.
Now the question comes out because for the example, a contradiction cannot be shown by using binary resolution and my question is: why? I mean, what is the practical way to show it?
I try to explain better what I want to say. Suppose we have to prove that:
$(A \lor B) \vdash_{R} (A \wedge B)$. By means of propositional resolution the process will be:
- convert in CNF and negate the "implication"; I mean we have to convert something of the form $\alpha \Rightarrow \beta $ into something of the form $\alpha \wedge \lnot \beta$ (that is the contrary of an implication). In our example we have the following set of clauses now:
{$(A \lor B),(\lnot A \lor \lnot B)$}.
- In this phase we have to apply resolution step which means that we have to try to detect some complementary literals to simplify. Well, let's consider our two clauses, we have two possible ways: we can consider A or also B (it's the same). In both cases we can never generate an empty clause that would mean to show that the negation of the original implication is unsatisfiable and therefore that the original entailment is satisfiable. In fact, you could generate two clauses $(B \lor \lnot B)$ or $(A \lor \lnot A)$ that are not contradictions. That's what I want to say.
Your counter-example is not a counter-example. What you are calling "binary resolution", which is just the standard resolution rule, is complete for first-order logic. The reason it fails to prove your proposed counter-example: $$ (\exists u \exists v (P(u) \wedge P(v)) \Rightarrow (\forall x \forall y (P(x) \lor P(y))) \tag*{(*)} ) $$ is because the above senetence is not valid, as may be seen by taking $P(x) \equiv x = 0$ over the domain of natural numbers.
Moreover, your attempt to show that $\mbox{(*)}$ cannot be proved by resolution is incorrect. In prenex-CNF form, the negation of $\mbox{(*)}$ is $$ \exists x\exists y\exists c\exists d(\lnot P(x) \land \lnot P(y) \land P(c) \land P(d)) $$ and not what you think it is: $$ \exists c\exists d \forall x \forall y((P(x) \lor P(y)) \land (\lnot P(c) \lor \lnot P(d)) $$
But as it happens resolution cannot derive a contradiction from either of these because they are both satisfiable. However, this does not contradict the completeness of resolution.
To expand on the propositional example you have added to your question: $A\lor B \vdash A \land B$ is not valid (take $A$ true and $B$ false). That's why the resolution rule can't prove it. This does not contradict the completeness of resolution.