# formal proof with natural deduction

Hi I am looking to prove

$r\wedge q\Leftrightarrow r \vdash r\Rightarrow q$

using natural deduction

I get:

• $r\wedge q\Leftrightarrow r$, assumption
• $r\vdash q$
• $r$, assumption

I assume that I also need to formally prove $q$ but cant figure out how to do it(and what rule would I use?) Am I correct so far? thank you.

• Is there any typo in $r\wedge q\Leftrightarrow p$? Maybe you meant $r$ instead of $p$? And also, is it $r\wedge (q\Leftrightarrow p)$ or $(r\wedge q)\Leftrightarrow p$? – frabala Feb 26 '14 at 17:20
• yes sorry i have fixed it – user131673 Feb 26 '14 at 17:23
• Are you attending same class or have you crated duplicate user to post duplicate post? math.stackexchange.com/questions/691161/formal-proof-logic – Trismegistos Feb 27 '14 at 8:36

(1) Assume $r$.

Then from the premise $(r\land q) \longleftrightarrow r$, which means $((r\land q)\rightarrow r)\land (r\rightarrow (r\land q))$, we have

(2) $r\rightarrow (r\land q)$,

Since $r$ is assumed, we have, by modus ponens using $(1), (2)$, we have

(3) $r\land q$.

This gives us, from (3),

(4) $q$.

From the assumption of $r$, we've deduced $q$.

Therefore, $r\rightarrow q$.

• sorry I am still confused how you get to r→(r∧q). is this derived by implication introduction? To do this do you not have to prove (r∧q) on its own? – user131673 Feb 26 '14 at 17:32
• @user131673 It's $\to \text{elimination}$ that is used. – Git Gud Feb 26 '14 at 17:34
• Actually, we use biconditional elimination in defining $(r\land q)\iff r$ to be the conjunction of two implications, $((r\land q)\rightarrow r)\land (r\rightarrow (r\land q))$, and then use "and"-elimination to get the implication we want: $r\rightarrow (r\land q).$ With $r$ as an assumption then, by using $\rightarrow$-elimination, we get $r\land q$... – Namaste Feb 26 '14 at 17:36
• thank you very much. apologies again, i am thick with a capital T. I worked this out. is this also valid: 1. p∧q⇔p assumption 2. r⇒r∧q,⇔Elimination, 1 3. r turnstile p∧q √ 3.1 r, assumption, 3 3.2 r, ∧Elimination,3 3.3 r⇒q, ⇒Introduction. 3.1,3.2 – user131673 Feb 26 '14 at 18:15
• thank you again, you have been a big help – user131673 Feb 26 '14 at 18:47