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

196 Views Asked by At

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.

1

There are 1 best solutions below

0
On BEST ANSWER

After the line "B −⇒e1 4", use disjunction introduction, perhaps labeled as vI, to derive "¬A ∨ B". That gives you what you want to show for the "A" case.

For the "¬A" case, use disjunction introduction to derive the same result you obtained in the other case, "¬A ∨ B". This takes care of the "¬A" case.

Since in both cases you reached the same result and indeed you obtained the result you were looking for, you can use disjunction elimination, perhaps labeled as vE, referencing the second line with the L.E.M. disjunction, and the lines associated with the two cases. That should complete the proof.