In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B?
I believe I need to assume A and do something Elim V, but I am really stumped as to what to do exactly. Any help would be appreciated.
In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B?
I believe I need to assume A and do something Elim V, but I am really stumped as to what to do exactly. Any help would be appreciated.
What do you mean by "corresponds to"?
To prove (~A v B) -> (A -> B), assume ~A v B and A and do Elim V on ~A v B. If ~A, then you get get a contradiction with A, so you can derive B by ex falso. Otherwise, you already have B.
To prove the converse implication is a little more difficult and requires double negation elimination.
Usually natural deduction is presented with the following two rules:
$\displaystyle \frac{\bot}{A}\bot\ \mbox{Elim}$ and $\displaystyle \frac{\neg\neg A}{A}\mbox{DNE}$ (double-negation elimination, called $\displaystyle \neg$ Elim in your program) for all formulas $\displaystyle A$
The rule $\displaystyle \bot$ Elim can be derived from DNE, which is what you did in your derivation:
Here the assumption ~B can be vacuous, in which case you derive B just from $\displaystyle \bot$.Code:~B Assumption ... _|_ _|_ Intro ~~B ~ Intro B DNE
The reason to keep these two rules separate is that the logic without DNE is quite interesting on its own.
Which program do you use to create Fitch-style derivations?