I need to provide a formal proof of the following argument:
Premise: $\exists x[P(X)\land\forall y(Q(y) \to \lnot R(x,y))]$
Premise: $\forall x[P(x) \to \forall y(S(y) \to R(x,y))]$
Conclusion: $\forall x(Q(x) \to \lnot S(x))$
I know there are rules of formal deduction but I am not exactly sure how to tackle this or which one I should use. Does anyone know how to solve this? Thanks!
Let $x_0$ be such that $$[P(x_0)\land\forall y(Q(y) \to \lnot R(x_0,y))].\tag{1} $$ Instantiating the 2nd premise with $x_0$ gives $[P(x_0) \to \forall y(S(y) \to R(x_0,y))]$, or, by using the contrapositive, equivalently $$ [P(x_0) \to \forall y(\neg R(x_0,y) \to \neg S(y))] \tag{2} $$ By (1), we know that $[P(x_0)$, so by Modus Ponens and (2) we can infer $$ \forall y(\neg R(x_0,y) \to \neg S(y))\tag{3} $$ Also from (1) we know that $$ \forall y(Q(y) \to \lnot R(x_0,y)) \tag{4} $$ Putting (3) and (4) together in a syllogism gives: $$ \forall y(Q(y) \to \lnot S(y)). \tag{Result} $$ Renaming the variable $y$ to $x$ gives the exact desired conclusion.