1
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – prime4567 May 9 at 11:55
  • $\begingroup$ Thanks for the advice :) $\endgroup$ – zzxxx123 May 9 at 12:02
  • 2
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA May 9 at 12:45
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.