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

Question

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?

Answer 1

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.

Answer 2

$(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)$