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

logicnatural-deductionpropositional-calculus

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$

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

Related Question