# Derive C V ~A

• Mar 20th 2012, 10:18 PM
divinelogos
Derive C V ~A
1| A⊃(B ∧ ~C) ASS
2| C V ~ B ASS

So far I have:

1| A⊃(B ∧ ~C) ASS
2| C V ~ B ASS
3 |A ASS/⊃E
4 |B ∧ ~C 1,3⊃E
5 |B 4, ∧E
6 |~C 4, ∧E

I'm not sure how to progress from here. I tried disjunction intro. on the next line to get ~C V ~B but it didn't help. Any ideas would be appreciated!
• Mar 21st 2012, 07:49 AM
emakarov
Re: Derive C V ~A
To continue your proof, use disjunction elimination (reasoning by cases) on C \/ ~B. Assuming either C or ~B leads to contradiction with formulas in steps 5 and 6. So, in fact, from 1 and 2 you can derive ~A, which is stronger than C \/ ~A.
• Mar 21st 2012, 05:26 PM
divinelogos
Re: Derive C V ~A
The problem is, I see the contradction, but I don't know how to write it out syntactically correct with the rules. Do I assume C or ~B for the purposes of negation introduction?
• Mar 21st 2012, 05:42 PM
emakarov
Re: Derive C V ~A
At this point it would be nice if you specified the proof system you are using, according to this sticky thread. My guess that it is Fitch-style natural deduction. Do you have the description of the marks on the right, such as ASS/⊃E? Also, are you familiar with the disjunction elimination rule?

Quote:

Do I assume C or ~B for the purposes of negation introduction?
Both in turn using disjunction elimination.
• Mar 21st 2012, 08:24 PM
divinelogos
Re: Derive C V ~A
The book calls the system "SD", and refers to it as a "derivation system". What do you mean by the description? For example, ASS/⊃E means assumption for the purposes of conditional elimination, if that's what you mean.
• Mar 22nd 2012, 08:52 AM
emakarov
Re: Derive C V ~A
It sure is not easy to extract information from you (Smile) Which book are you using? (I am interested to know anyway, but I won't be able to consult it to see the description of the proof system unless it is online.) Also, you have not said if you understand disjunction elimination, which is important in this example.

Here is my best guess about the complete derivation.
Code:

``` 1| C ∨ ~B ASS  2|| C ASS/∨E  3|| A ⊃ (B ∧ ~C) ASS  4||| A ASS/~I  5||| B ∧ ~C 4,3⊃E  6||| ~C 5∧E  7|| ~A 4,2,6~I  8|| ~B ASS/∨E  9|| A ⊃ (B ∧ ~C) ASS 10||| A ASS/~I 11||| B ∧ ~C 10,11⊃E 12||| B 11∧E 13|| ~A 10,12,8~I 14| ~A 1,2,7,8,13∨E 15| C ∨ ~A 14∨I```
I prefer a tree presentation of the derivation. Here closed assumptions are labeled with step numbers in the derivation above where these assumptions are introduced. Similarly, rules that close assumptions (~I and ∨E) are labeled with the assumptions' numbers.