3
$\begingroup$

This question already has an answer here:

I could easily prove

$\neg P \lor Q$ entails $P \rightarrow Q$.

It is well known that

$P \rightarrow Q$ entails $\neg P \lor Q$

but I couldn't find a way to prove it.

Although there is the same question; How to prove that $P \rightarrow Q$ is equivalent with $\neg P \lor Q $?; it's a little bit confusing and I need to see step by step solution.

Could you show me the way by using Natural Deduction?

$\endgroup$

marked as duplicate by Git Gud, Namaste, Chris Janjigian, Carl Mummert, Vladimir Reshetnikov Nov 2 '14 at 17:57

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

3
$\begingroup$

Assume : $P \rightarrow Q$ --- premise

1) $\lnot (\lnot P \lor Q)$ --- assumed [a]

2) $\lnot P$ --- assumed [b]

3) $\lnot P \lor Q$ --- from 2) by $\lor$I

4) $\bot$ --- from 1) and 3) by $\lnot$E (or $\rightarrow$E)

5) $P$ --- from 2) and 4) by Double Negation, discharging [b]

6) $Q$ --- from premise and 5) by $\rightarrow$E

7) $\lnot P \lor Q$ --- from 6) by $\lor$I

8) $\bot$ --- from 1) and 7) by $\lnot$E (or $\rightarrow$E)

9) $\lnot P \lor Q$ --- from 1) and 8) by Double Negation, discharging [a]

Thus :

$P \rightarrow Q \vdash \lnot P \lor Q$.

$\endgroup$
  • $\begingroup$ thank you mauro, but i couldn't understand the implication elimination in contradiction lines(4,8). which implication we eliminate? $\endgroup$ – Cnqt Nov 2 '14 at 17:29
  • $\begingroup$ @Cnqt - perhaps you know the rule $\lnot$E : from $\varphi, \lnot \varphi$, infer $\bot$; I've applied this rule in the form : $\lnot \varphi := \varphi \rightarrow \bot$. Assuming this abbreviation, the above rule is from $\varphi, \varphi \rightarrow \bot$, infer $\bot$, taht is simply an application of $\rightarrow$E. $\endgroup$ – Mauro ALLEGRANZA Nov 2 '14 at 17:57

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