I'm having trouble solving this formal proof in Fitch. I've put together most of it, but I think I need to use disjunction elim(?) at some point and am having trouble doing that.
1 Answer
So very close.
You have all the pieces for this, but you wandered off the path along the way.
You knew to seek to derive Small(b) under the assumption of Small(c). You immediately derived Small(d) v Small(e) and correctly decided to eliminate this disjunction... then apparently forgot where you wanted to go.
Always keep an eye on the destination.
The first case of Small(d) should have derived Small(b) by contradiction elimination .
The second case of Small(e) must aim for the same; and here what you needed to do was nest a second disjunction elimination. The disjunction to eliminate is the first premise, Small(b) v Cube(b) -- the first case is trivial, and the second case I am sure that you can do, so...
| Small(b) v Cube(b) P
| Small(c) > Small(d) v Small(e) P
| Small(d) > ~Small(c) P
|_ Cube(b) > ~Small(e) P
| |_ Small(c) A
| | Small(d) v Small(e) >E
| | |_ Small(d) A
| | | ~Small(c) >E
| | | # #I <- you had it up to here
| | | Small(b) #E <- derive this instead
| | +
| | |_ Small(e) A
| | | Small(b) v Cube(b) R <- the first premise
| | | |_ Small(b) A
| | | | Small(b) R
| | | +
| | | |_ Cube(b) A
| | | | : :
| | | | Small(b) .
| | | Small(b) vE
| | Small(b) vE
| Small(c) > Small(b) >I
