From this set of rules:
$ (\wedge E) $ $A \wedge B \vdash A $
$ (\wedge I) $ $A, B \vdash A \wedge B $
$ (\vee E) $ $ A \vee B, A \rightarrow C, B \rightarrow C \vdash C $
$ (\vee I) $ $ A \vdash A \vee B $
$ (\neg E) $ $ \neg A \rightarrow B, \neg A \rightarrow \neg B \vdash A $
$ (\neg I) $ $ A \rightarrow B, A \rightarrow \neg B \vdash \neg A $
$ (\rightarrow E) $ $ A, A \rightarrow B \vdash B $
$ (\rightarrow I) $ $ Premises \vdash A \rightarrow B $
With the last rule ($ \rightarrow I $), you can introduce any implication you like as long as you prove in a sub-proof the consequent of the implication under the assumption of the hypothesis of the implication e.g.
- $ P \rightarrow Q \quad $ Premise
- $ \neg Q \quad\quad\space\space $ Premise
- $ P \rightarrow \neg Q \quad \rightarrow I,$ subproof below
3.1 $ P \quad\space\space\space $ Assumption
3.2 $ \neg Q \quad $ from (2) - $ \neg P \quad $ from (1)(3), $ \neg I $
Prove $ A \rightarrow B \vdash \neg A \vee B $
I know I need to get $ \neg A $ or $ B $ or $ A $ (and thus B via $ A \rightarrow B) $ to prove the conclusion via ($ \vee I $) but I can't seem to get any of those.
Here is one of my better attempts but I get stuck at line (2.3.2) as I can't see a way to get $\neg A$:
- $ A \rightarrow B \quad $ Premise
- $ A \rightarrow \neg B \quad \rightarrow I $ , subproof below
2.1 $ A \quad\quad\quad $ Assumption
2.2 $ B \rightarrow A \quad \rightarrow I $ , subproof below
$\quad$ 2.2.1 $ B \quad $ Assumption
$\quad$ 2.2.2 $ A \quad $ from (2.1)
2.3 $ B \rightarrow \neg A \quad \rightarrow I $ , subproof below
$\quad$ 2.3.1 B $ \quad $ Assumption
$\quad$ 2.3.2 ???
If I had been able to get $ \neg A $ then I could of got $ \neg B $ on line (2.4) via ($\neg I$) and thus $ \neg A $ on line (3) also via ($\neg I$) and the conclusion $ \neg A \vee B $ on line (4) via ($\vee I$).
Any suggestions on how to prove this?
Edit:
Thanks everyone, I am now able to prove it I think:
Prove $ A \rightarrow B \vdash \neg A \vee B $
- $ A \rightarrow B \quad $ Premise
- $ \neg (\neg A \vee B) \rightarrow (\neg A \vee B) \quad \rightarrow I $, subproof below
2.1 $ \neg (\neg A \vee B) \quad $ Assumption
2.2 $\neg A \rightarrow (\neg A \vee B) \quad \rightarrow I $, subproof below
$\quad$ 2.2.1 $\neg A \quad\quad\quad\quad $ Assumption
$\quad$ 2.2.2 $\neg A \vee B \quad\quad $ (2.2.1), $\vee I$
2.3 $\neg A \rightarrow \neg (\neg A \vee B) \quad \rightarrow I $, subproof below
$\quad$ 2.3.1 $ \neg A \quad\quad\quad\quad $ Assumption
$\quad$ 2.3.2 $ \neg (\neg A \vee B) \quad $ (2.1)
2.4 $ A \quad\quad\quad $ (2.2)(2.3), $\neg E$
2.5 $ B \quad\quad\quad $ (2.4)(1), $\rightarrow E $
2.6 $ \neg A \vee B \quad $ (2.5), $\vee I $ - $\neg (\neg A \vee B) \rightarrow \neg (\neg A \vee B) \quad \rightarrow I $, subproof below
3.1 $\neg (\neg A \vee B) \quad $ Assumption
3.2 $\neg (\neg A \vee B) \quad $ (3.1) - $ \neg A \vee B \quad $ (2)(3), $\neg E$
Best Answer
Hint
You need $\lnot B \lor B$.
From it, by $\lor$-Elim you have two cases:
(i) $B$ and then $\lnot A \lor B$.
(ii) $\lnot B$. Assume $A$ and derive a contradiction. Thus derive $\lnot A$ discharging the assumption, and finally derive $\lnot A \lor B$.