Proving $\exists x\lnot R(x), \forall x(P(x)\to Q(x)), \forall x(\lnot Q(x) \lor R(x)) \vdash \exists x\lnot P(x)$

Question

This is the proof we have to prove: $$\exists x\lnot R(x), \forall x(P(x)\to Q(x)), \forall x(\lnot Q(x) \lor R(x)) \vdash \exists x\lnot P(x)$$

My proof:

1. $∀x(P(x)→Q(x))$ From data

2. $∃x¬R(x)$ From data

3. $∀x(¬Q(x) ∨ R(x))$ From data

4. $¬R(a)$ 2. and ∃-E

5. $P(a)→Q(a)$ 1. and ∀-E

6. $¬Q(a) ∨ R(a)$ 3. and ∀-E

7. $¬Q(a)$ 4., 6., and vE2.

8. $P(a)→¬Q(a)$ 5., 8., and ¬I

9. $¬P(a)$ From sub computation box

10. $∃x¬P(x)$ 9. and ∃-I

Is my proof correct? I am unsure about line 8. in particular

These are the rules we use:

Answer 1

My proof:

The rules are an older version of natural deduction, so are a bit unfamiliar. But it looks mostly okay.

$~$ 1. $∀x(P(x)→Q(x))$ From data

$~$ 2. $∃x¬R(x)$ From data

$~$ 3. $∀x(¬Q(x) ∨ R(x))$ From data

$~$ 4. $¬R(a)$ 2. and ∃-E

That is not typically how existential elimination is used, but I have seen it so in older text, so maybe yours does. Please check your reference.

$~$ 5. $P(a)→Q(a)$ 1. and ∀-E

$\quad$ 6. $¬Q(a) ∨ R(a)$ 3. and ∀-E

$\quad$ 7. $¬Q(a)$ 4., 6., and vE2.

$~$ 8. $P(a)→¬Q(a)$ 5., 8., and ¬I

This should be derived using $\to\mathsf I$ . So raise a 'sub computation box' with the assumption of $P(a)$ just before line 6 .

$~$ 9. $¬P(a)$ From sub computation box

Now, this is where $\lnot\mathsf I$ is used, calling $5$ and $8$.

$~$ 10. $∃x¬P(x)$ 9. and ∃-I

---

$$\boxed{\begin{array}{l}~~1.~~\forall x~(P(x)\to Q(x))\\~~2.~~\exists x~\lnot R(x)\\~~3.~~\forall x~(\lnot Q(x)\vee R(x)\\\hline{~~4.~~\lnot R(a)\hspace{20ex}2, \exists{-}\mathsf E\\~~5.~~P(a)\to Q(a)\hspace{13ex} 1, \forall{-}\mathsf E\\\quad\boxed{\begin{array}{l}5.1.~~P(a)\\\hline{~~6.~~\lnot Q(a)\vee R(a)\hspace{9ex} 3, \forall{-}\mathsf E\\~~7.~~\lnot Q(a)\hspace{16ex} 4, 6,\vee{-}\mathsf E2}\end{array}}\\~~8.~~P(a)\to\lnot Q(a)\hspace{11ex}5a{-}7,{\to}{-}\mathsf I\\~~9.~~\lnot P(a)\hspace{20ex} 5, 8, \lnot{-}\mathsf I\\10.~~\exists x~\lnot P(x)\hspace{17ex} 9, \exists{-}\mathsf I}\end{array}}$$

Answer 2

Your step 8 has to be wrong because it depends on itself. Try applying rule $\rightarrow$I2 to rule 7 instead. Then there will be a negation rule that applies to 5 and 8 (there is no computation box).