How to prove two statements given axioms

Question

I have no idea what to do or what kind of proof to use for this. Please help.

Given the following axioms:

a.∀x (P(x)→ R(x))

b.Ǝx (¬R(x)∧ Q(x))

Prove: Ǝx (Q(x)∧ ¬P(x)).

Show the rules of inference (and prior steps) used at each step:

This is what I have tried but I don't think this is correct

$\begin{array}{ll}\text{Assume}&\exists x~(\lnot R(x)\land Q(x))\\ \text{since}&\exists x~\lnot R(x)\\ & \lnot R(x)\\ \text{because}& P(x) \to R(x)\\ \text{but}& \forall x~ (P(x) \to R(x))\\ \text{this is a contradiction so}& \exists x~(\lnot R(x)\land Q(x))\text{ is false} \end{array}$

Answer 1

$\neg R(c)$ does not contradict $P(c)\to R(c)$.   Recall that a conditional is true if the consequent is true or the antecedent is false.   So if you deny the consequent, you assert the antecedent is false.   That is, you use the rule of modus tollens.

$\boxed{\begin{array}{l|l:rlr}1 & \forall x~(P(x)\to R(x)) && \text{Premise} \\ 2 & \exists x~(\lnot R(x)\land Q(x)) && \text{Premise} \\\hdashline \quad 3 & \lnot R(c)\wedge Q(c) &2& \text{Assumption (for Existential Elimination)} & \text{Witness } c\\ \quad 4 & \lnot R(c) & 3 & \text{Conjunctive Elimination} \\ \quad 5 & P(c)\to R(c) &1& \text{Universal Elimination} \\ \quad 6 & \color{red}{\lnot P(c)} & 4,5 & \text{Consequent Denial} & \text{(modus tollens)} \\ \quad 7 & & & \\ \quad 8 & & &\\\quad 9 &&& \\ \hline 10 & \exists x~(Q(x)\wedge \lnot P(x)) & 2,3{-}9 &\text{Existential Elimination} & \text{Discharge }c \end{array}}\\\therefore \qquad \forall x~(P(x)\to R(x)), \exists x~(\lnot R(x)\vee Q(x))~\vdash~ \exists x~(Q(x)\wedge \lnot P(x))$

Fill in the remaining steps to complete the proof.

Answer 2

Just a different style:

01 ∀x[P(x)→R(x)]       premise
02 ∃x[¬R(x)∧Q(x)]      premise
  03 ¬R(a)∧Q(a)        assumption
  04 ¬R(a)             ∧elim 03
  05 Q(a)              ∧elim 03
    06 P(a)            assumption
    07 P(a)→R(a)       ∀elim 01 a/x
    08 R(a)            →elim 07 06
    09 ⊥               contradiction 08 04
  10 ¬P(a)             ¬intro 06-09
  11 Q(a)∧¬P(a)        ∧intro 05 10
  12 ∃x[Q(x)∧¬P(x)]    ∃intro 11 x/a
13 ∃x[Q(x)∧¬P(x)]      ∃elim 02 03-12