I'm in desperate need of some pointers for my logic homework due in tomorrow. It's disjunction elimination and I'm completely stuck.
These are the premises - A ∨ (B∧C). ¬B∨¬C∨ D. And I have to derive A ∨ D
So I can see why it has to be either A or D, because if its B and C, then it cannot be ¬B or ¬C so must be D. And if its not B and C, then it has to be A. But I cant work out how to show that using formal proofs in the fitch system. I'm getting stuck on how to do disjunction elimination with two premises
And for the second question - I have these premises ¬(¬Cube(a)∧Cube(b)) ¬(¬Cube(b)∨Cube(c)).
and have to derive Cube(a). Again I can formulate in words a reason as to why this is the case. But I don't even know where to begin in terms of a formal derivation.
Any pointers/advice would be greatly appreciated
First you do two subproofs to set up a disjunction elimnation for $A \lor (B \land C)$: one that assumes $A$, and one that assumes $B \land C$. In both cases, you want the last line of the subproof to be $A \lor D$.
Ok, so for the first subproof that is easy: just use disjunction introduction to derive $A \lor D$ from $A$.
For the second subproof, you want of course derive $D$, so that you can then use disjunction introduction as well to get $A \lor D$ ... and, obviously, you want to use the second premise to get to $D$ ... but how?
Well, you are going to have to set up another disjunction elimination, but this time for the second premise, and you do it inside the subproof that assumed $B \land C$. That is, you create three new subproofs inside the second subproof: one that assumes $\neg B$, one that assumes $\neg C$, and one that asssumes $D$. In each case, you once again want to have $A \lor D$ as the last line of the subproof.
Now, for the subproof with $D$ that is easy, bit how do you do this for $\neg B$ and $\neg C$? Well, remember that you are doing these three subproofs inside the subproof for $B \land C$. So, you can use that assumption. In particular, using elimination you can get both $B$ and $C$ by themselves. Therefore, you can derive a contradiction from $B$ and $\neg B$ inside the subproof with $B$ using contradiction introduction. And, from a contradiction you can infer anything you want using contradiction elimnation ... and of course what you want to infer is $A \lor D$. Same for $C$ ... and then it is just a matter of wrapping up!