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.


  • $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Mar 2 '16 at 16:18
  • $\begingroup$ 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 $\endgroup$ – amiAI Mar 2 '16 at 16:22
  • $\begingroup$ 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$"? $\endgroup$ – la flaca Mar 2 '16 at 16:27
  • $\begingroup$ The |- symbol represents a syntactic turnstile. The 3rd line is the assertion that p will imply q once proved. $\endgroup$ – amiAI Mar 2 '16 at 16:31
  • $\begingroup$ @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. $\endgroup$ – 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$.


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.