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?


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.


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$.

  • $\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.