Trying to check whether a formal proof is correct

Question

Am having a little difficulty trying to formally prove a formula. I'm new to this so just trying to have a go and see where I get to. The formula I have is copied in below;

     p ∧ r ⇒ q ∧ r , p ∨ r ⇒ q ∨ r |- p ⇒ q

I have had a go at it but I don't really know if I'm correct. I would be really grateful if someone could check for me.

    1. p ∧ r ⇒ q ∧ r    Assumption 0
    2. p ∨ r ⇒ q ∨ r    Assumption 0
    3. p |- q   
   3.1 p                 Assumption 3
   3.2 r                 ∧-E from Line 1
   3.3 q                 ⇒-E from Line 1 & 2
    4. p ⇒ q             ⇒-I from Line 3.1 & 3.3

I would really appreciate it if anyone could show me if I'm going wrong. I'm not sure at all if I'm right or wrong.

Thanks.

Answer 1

1) $p ∧ r → q ∧ r$ --- premise

2) $p ∨ r → q ∨ r$ --- premise

3) $p$ --- assumed [a]

4) $p ∨ r$ --- from 3) by $∨$-I

5) $q ∨ r$ --- from 4) and 2) by $→$-E.

Now we need $∨$-E (proof by cases) from 5):

6) $q$ --- assumed [b]

7) $p → q$ --- from 3) and 6) by $→$-I

8) $r$ --- assumed [c]

9) $p ∧ r$ --- from 3) and 8) by $∧$-I

10) $q ∧ r$ --- from 1) and 9) by $→$-E

11) $q$ --- from 10) by $∧$-E

12) $p → q$ --- from 3) and 11) by $→$-I.

Having derived $p → q$ from both 6) and 8), we can apply $∨$-E to 6)-7) and 8)-12) and 5), discharging [b] and [c], to conclude with:

$p → q$.

Thus:

$p ∧ r → q ∧ r, p ∨ r → q ∨ r \vdash p → q$.

Answer 2

Your line 3.2 is wrong. You can't apply $\land$-elimination to line 1, because line 1 does not have $\land$ as its top-level connective; it should be parenthesized as $(p\land r)\Rightarrow(q\land r)$.

Line 3.2 is wrong too; neither of line 1 and 2 is identical to the left-hand side of the other wone. And in any case $q$ is not the right-hand side of either of 1 and 2; $\Rightarrow$-elimination can only conclude a formula that is to the right of a $\Rightarrow$ in its first premise.

---

It would probably help if you formulate a proof in informal English before you try writing down a formal one. It would go something like:

Since we have $p$, in particular $p\lor r$ and therefore, by the second assumption $q\lor r$. If $q$ is true, then we're done already; otherwise $r$ is true, so we have $p\land r$, and therefore by the first assumption $q\land r$. So in this case too, $q$ will hold.