if $\forall x\forall y[P(x) \land P(y) \implies Q(x,y)]$ then prove that $\forall y \exists x[P(x)\land \lnot Q(x,y) \implies \lnot P(y)]$

Question

I was solving a past paper for my first discrete math course in preparation for my first discrete math exam and I found this question and I had absolutely no idea what to do.

Answer 1

Hint

With Natural Deduction it is quite easy.

With Rosen's proof system the proof is a little bit tricky.

Proof sketch:

Remove the leading quantifiers using Universal instantiation (page 76) to get:

$(P(x) ∧ P(y)) \to Q(x,y)$.

The apply the rule: "replace the conditional statement $p → q$ with the equivalent disjunction ¬$p ∨ q$ (page 74: resolution)" and use De Morgan to get:

$\lnot P(x) \lor \lnot P(y) \lor Q(x,y)$.

Now rewrite it as:

$\lnot P(x) \lor Q(x,y) \lor \lnot P(y)$

and use De Morgan and the equivalence above again to get:

$(P(x) \land \lnot Q(x,y)) \to \lnot P(y)$.

Now use Existential generalization followed by Universal generalization (page 76) to get:

$∀y∃x[(P(x) ∧ ¬Q(x,y)) \to ¬P(y)]$.

---

You can consider also onother possible "propositional transformation": $(p_1 \land p_2) \to q$ is equivalent to $p_1 \to (p_2 \to q)$ and $(p_2 \to q)$ is equivalent to $(\lnot q \to \lnot p_2)$.

Thus, we have that $(p_1 \land p_2) \to q$ is equivalent to: $(p_1 \land \lnot q) \to \lnot p_2$.