# Trying to check whether a formal proof is correct

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.

• Line 1 is $p \land r \to q \land r$; thus, assuming only $p$, there is no way to use $\land$-E to derive $r$ from it. – Mauro ALLEGRANZA Mar 2 '16 at 16:18
• okay - if I remove the line to derive r; does it still work? or am I completely wrong here? really appreciate your help Mauro! @MauroALLEGRANZA – amiAI Mar 2 '16 at 16:22
• The first two lines of your deduction are your premises but where does the third line comes from? And what does it mean "p|-q" in this context? Should it be understood as "$p \implies q$"? – la flaca Mar 2 '16 at 16:27
• The |- symbol represents a syntactic turnstile. The 3rd line is the assertion that p will imply q once proved. – amiAI Mar 2 '16 at 16:31
• @SamNeeds: I'm 80% sure you're not supposed to write $p\vdash q$ down as a separate line in the particular proof notation you're working with. – hmakholm left over Monica Mar 2 '16 at 16:36

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.

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$.