# Proving the sequent $A \implies B \vdash \lnot A \lor B$ using natural deduction

When proving the sequent $$A ⇒ B ├ \ ¬A ∨ B$$, my first approach was to try and use the Law of excluded middle:
$$A ⇒ B - Premise \ 1\\ A V ¬A \ -L.E.M \ 2\\ \ \ \ \ \ \ \ A \ - assume \ 3 \\ \ \ \ \ \ \ \ B \ - ⇒e1 \ 4 \\ \ \ \ \ \ \ \ ¬A \ - assume \ 5 \\$$

But I'm not really sure where to go from here, as it doesn't seem correct. Maybe there is a more fundamental approach. Any pointers or tips would be appreciated, thanks.

• This is a good start. To get ~A, just use deductive syllogism if you're allowed: AvB, ~A |- B. In any case ((AvB) & ~A) ---> B is a tautology. Hope that helps. – prime4567 May 9 at 11:55
• Thanks for the advice :) – zzxxx123 May 9 at 12:02
• Good start. For ND use $\lor$-elim with $A \lor \lnot A$. In both cases you get $\lnot A \lor B$ and it's done. – Mauro ALLEGRANZA May 9 at 12:45