1
$\begingroup$

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?

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

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – user284003 Oct 26 '15 at 10:36
  • 1
    $\begingroup$ 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. $\endgroup$ – Henno Brandsma Oct 26 '15 at 10:45
  • $\begingroup$ oooh I see, thank you $\endgroup$ – user284003 Oct 26 '15 at 10:56
  • 1
    $\begingroup$ @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. $\endgroup$ – Mauro ALLEGRANZA Oct 26 '15 at 11:04
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – user284003 Oct 26 '15 at 9:44

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.