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.
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.
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?
Both in turn using disjunction elimination.Do I assume C or ~B for the purposes of negation introduction?
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.
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.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