Thread: 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!

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.

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?

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?

Do I assume C or ~B for the purposes of negation introduction?

Both in turn using disjunction elimination.

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.

It sure is not easy to extract information from you 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.