# 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
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}