Is a truth table not an acceptable proof for this? That's what I would use.
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.
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:
and (double-negation elimination, called Elim in your program) for all formulas
The rule 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 .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?