Deriving a implies b from (not a) or b (formally: $\neg a \vee b\vdash a\rightarrow b$)

Question

I've struggled a long time proving $\neg a \vee b\vdash a\rightarrow b$ via natural deduction, so I thought I can just show (and explain) how it's done after I finally figured it out.

Answer 1

Note that both formulae are even equivalent, so we could also show $ a\rightarrow b \vdash \neg a \vee b$, but here I only show the former case.

Since the premise is a disjunction it's quite obvious that we will need the disjunction elimination rule, which looks as follows:

Given:
- $X\vdash A\vee B$,
- $Y,A\vdash C$, and
- $Z,B\vdash C$,
we can derive $X,Y,Z\vdash C$ ($\vee E$), which discharges $A$ from $Y,A$ and $B$ from $Z,B$.

To make the following proof shorter, I will also use the rule RAA (reductio ad absurdum), which is nothing else than a "compact representation" (i.e., concatenation/combination) of negation elimination (introducting a contradiction symbol from two contradicting assumptions) plus negation introduction (which introduced the negation of an assumption given a contradiction). Formally:

Given:
- $X,B\vdash A$ and
- $Y,B\vdash \neg A$
we can conclude $X,Y\vdash \neg B$ (RAA).

The proof uses the following format:
col 1 = assumptions,
col 2 = line number,
col 3 = derived formula,
col 4 = the numbers used are all line numbers, except for numbers in "[]", which are the assumption numbers that get discharged

We want to show: $\neg a \vee b\vdash a\rightarrow b$ \begin{align*} 1 & &(1) & &\neg A \vee B & &A\\ 2 & &(2) & &A & &A\\ 3 & &(3) & &\neg A & &A\\ 4 & &(4) & &B & &A\\ 2,3 & &(5) & &\neg\neg B & &RAA\ 2,3[]\\ 2,3 & &(6) & &B & &\neg\neg{}E\ 5\\ 1,2 & &(7) & &B & &\vee{}E\ 1,4[4],6[3]\\ 1 & &(8) & &A\rightarrow B & &\rightarrow{}I\ 7[2] \end{align*}

Note that the proof uses an empy discharge in line (5). Here, 2,3[] simply means that the assumption that we are discharching has not been explicitly made and that we thus also do not depend on this assumption. The assumption that we are "discharging" here is $\neg B$, but since we didn't actually need this, we do not have a line and assumption number for it, thus the empty brackets.

Answer 2

Let me write the truth table;

$a$| $b$ | $-aVb$ | $a\rightarrow b$| $(-aVb)\rightarrow (a\rightarrow b)$

|T | T | T | T| T

|T | F | F | F| T

|F| | T | T | T| T

|F | F | T | T| T

Truth values in the last column gives the desired conclusion.

Answer 3

Using a form of natural deduction ('|' = OR), and assuming you can't just use the standard definition of implication: