Prove $A \rightarrow B \vdash \neg A \vee B$, using Natural Deduction

Question

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.

1. $ P \rightarrow Q \quad $ Premise
2. $ \neg Q \quad\quad\space\space $ Premise
3. $ P \rightarrow \neg Q \quad \rightarrow I,$ subproof below
   3.1 $ P \quad\space\space\space $ Assumption
   3.2 $ \neg Q \quad $ from (2)
4. $ \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$:

1. $ A \rightarrow B \quad $ Premise
2. $ 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 $

1. $ A \rightarrow B \quad $ Premise
2. $ \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 $
3. $\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)
4. $ \neg A \vee B \quad $ (2)(3), $\neg E$

Answer 1

The rules you need are:

• $({\to}\mathsf E)\quad A, A\to B \vdash B$
• $(\mathsf A)\quad\neg (\neg A\lor B)\vdash\neg (\neg A\lor B)$
• $(\lor\mathsf I)\quad\neg A\vdash \neg A\lor B$
• $(\lor\mathsf I)\quad B \vdash \neg A\lor B$

Begin with these assumptions

1. $A\to B\hspace{16.1ex}\text{Premise}$

   2. $\neg(\neg A\lor B)\hspace{8ex}\text{Assumption}$

      3. $\neg A\hspace{11.5ex}\text{Assumption}$

Answer 2

There isn't a rule of inference ($\lor$I) A $\vdash$ (B$\lor$A)?

If you have that rule, then assume A. Then you can infer B by (-> E). So, then ($\lnot$A $\lor$ B).

Assume $\lnot$A. Then ($\lnot$A $\lor$ B).

Then prove (A$\lor$$\lnot$A).

Then use ($\lor$E) to give you ($\lnot$A$\lor$B).

Answer 3

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$.

Answer 4

Perhaps, a possible proof using your system rules, could be: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

$ \fitch{1.\,A \to B}{ \fitch{2.\,\lnot(\lnot A \lor B)}{ \fitch{3.\,\lnot B}{ \fitch{4.\,A}{ 5.\,\lnot B \R{3} }\\ 6.\,A \to \lnot B \ii{4-5} 7.\,\lnot A \ni{1,6} 8.\,\lnot A \lor B \oi{7} }\\ 9.\,\lnot B \to (\lnot A \lor B) \ii{3-8} \fitch{10.\,\lnot B}{ 11.\,\lnot(\lnot A \lor B) \ie{9,10} }\\ 12.\,\lnot B \to \lnot(\lnot A \lor B) \ii{10-11} 13.\,B \ne{9,12} 14.\, \lnot A \lor B \oi{13} }\\ 15.\,\lnot(\lnot A \lor B) \to (\lnot A \lor B) \ii{2-14} \fitch{16.\,\lnot(\lnot A \lor B)}{ 17.\, \lnot(\lnot A \lor B) \R{16} }\\ 18.\,\lnot(\lnot A \lor B) \to \lnot(\lnot A \lor B) \ii{16-17} 19.\,\lnot A \lor B \ne{15,18} } $