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.

- Dec 6th 2011, 07:59 PMCDsIn formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
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. - Dec 6th 2011, 11:12 PMAnnatalaRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
Is a truth table not an acceptable proof for this? That's what I would use.

- Dec 7th 2011, 02:27 AMemakarovRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
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. - Dec 7th 2011, 03:46 AMprincepsRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
- Dec 7th 2011, 08:50 AMCDsRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
This is what I've done so far. It's how to get from step 5 to 6 that confuses me.

http://i1194.photobucket.com/albums/...ps29/Proof.jpg - Dec 7th 2011, 09:02 AMCDsRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
Nevermind, I figured it out. And I even know how to do the reverse. Thanks a lot guys!

- Dec 7th 2011, 09:10 AMemakarovRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
So, could you say how you derived B in step 6 for everybody's benefit?

- Dec 7th 2011, 04:59 PMCDsRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
Fitch says that I've proved what I tried to prove, yet upon more reflection I'm worried it might due to a bug in the program (view steps 6-9). Could somebody confirm if I did this properly?

Attachment 23042 - Dec 7th 2011, 10:13 PMemakarovRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
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:

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? - Dec 10th 2011, 01:23 PMCDsRe: In formal Logic (Fitch Format), how do I prove ~A v B corresponds to A -> B
The program is called Fitch by a CD called Language, Proof and Logic.