# (s → p) ∨ (t → q) entails (s → q) ∨ (t → p) natural deduction

Hey guys I am stuck on this proof $(s \rightarrow p) \lor (t \rightarrow q)$ entails $(s \rightarrow q) \lor (t \rightarrow p)$ using natural deduction to prove it.

I used the or elimination in order to split up the two brackets, but I can't get any further...

Can anybody help me out on this one?

• What exact rules are you allowed to use? Online reference? – Henno Brandsma Oct 26 '15 at 10:19

1) $(s → p) ∨ (t → q)$ --- premise

2) $(s → p)$ --- assumed [a1] for 1st $∨$-elim

3) $\vdash p \lor \lnot p$ --- LEM

4) $p$ --- assumed [b1] for 2nd $∨$-elim

5) $t \to p$ --- from 4) by $\to$-intro

7) $(s → q) ∨ (t → p)$ --- from 5) by $\lor$-intro

8) $\lnot p$ --- assumed [b2] for 2nd $∨$-elim

9) $s$ --- assumed [c]

10) $p$ --- from 9) and 2) by $\to$-elim

11) $\bot$ --- from 8) and 10)

12) $q$ --- from 11) by $\bot$-rule

13) $s \to q$ --- from 9) and 12) by $\to$-intro, discharging [c]

14) $(s → q) ∨ (t → p)$ --- from 13) by $\lor$-intro.

Now, from 4-7 and 8-14 and 3, by $\lor$-elim (the 2nd one) we derive :

15) $(s → q) ∨ (t → p)$ --- discharging temporary assumptions [b1] and [b2].

16) $(t → q)$ --- assumed [a2] for 1st $∨$-elim

and we have to repeat the same derivation above, concluding by $\lor$-elim (the 1st one) with :

17) $(s → q) ∨ (t → p)$ --- discharging temporary assumptions [a1] and [a2].

Thus :

$(s → p) ∨ (t → q) \vdash (s → q) ∨ (t → p)$ --- from 1), 2-15) and 16-17).

Note that the use of LEM in the proof has the role of the equivalence between $p \to q$ and $\lnot p \lor q$ (see other answer), in the sense that, in order to prove $(p \to q) \leftrightarrow (\lnot p \lor q)$ with Natural Deduction, we have to use rules like RAA or DN that are equivalent to LEM.

• Where does the t in step 5 come from? Don't I have to assume t and get to p in order to have t -> p? – user284003 Oct 26 '15 at 10:36
• You already have $p$. So formally, yes: you add an extra assumption $t$, as we have $p$ already, we immediately eleminate the asumption to get $t \rightarrow p$, as stated. This step is trivially added. – Henno Brandsma Oct 26 '15 at 10:45
• oooh I see, thank you – user284003 Oct 26 '15 at 10:56
• @user284003 - "intuitively", the move $p \vdash t \to p$ is licensed by the fact that $p \to (t \to p)$ is a tautology. The "machinery" is : (i) we have derived $p$; (ii) we assume $t$; (iii) we "reiterate $p$ (we have it already); (iv) we derive $t \to p$ discharging $t$. Thus : $p \vdash t \to p$. See for more details this post. – Mauro ALLEGRANZA Oct 26 '15 at 11:04

$(s → p) ∨ (t → q)$

$( \neg s ∨ p) ∨ (\neg t ∨ q)$

$\neg s ∨ p ∨ \neg t ∨ q$

$\neg t ∨ p ∨ \neg s ∨ q$

$(\neg s ∨ q) ∨ (\neg t ∨ p)$

$(s → q) ∨ (t → p)$

• Yeah that was my thought too, but I am not allowed to form s -> p into (not s OR p). I am only allowed to use rules of the natural deduction MP, MT etc...is there any other way? – user284003 Oct 26 '15 at 9:44