proof that p implies q entails not p or q [duplicate]

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 ReshetnikovNov 2 '14 at 17:57

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

• thank you mauro, but i couldn't understand the implication elimination in contradiction lines(4,8). which implication we eliminate? – Cnqt Nov 2 '14 at 17:29
• @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. – Mauro ALLEGRANZA Nov 2 '14 at 17:57