SD Logic Homework (Derivability)

[thefuturism]

The question is:

Show that the following derivability claim holds in SD.
(I'll use ">" to stand in for conditional.)

{(A > F) & (F > D), ((M v H) v C) > A, ~(M v H) & C} entails D

I'm only allowed to use the basic derivation rules of SD:
Reiteration (R)
Conjunction Intro. (&I) and Conjunction Elim. (&E)
Conditional Intro. (>I) and Conditional Elim. (>E)
Negation Intro. (~I) and Negation Elim. (~E)
Disjunction Intro. (vI) and Disjunction Elim. (vE)
Biconditional Intro. (triplebarI) and Biconditional Elim. (triplerbarE)

I've made numerous attempts at this problem, while growing more and more frustrated after each failure.
Here is what I believe to be my closest answer:

1. (A > F) & (F > D) [assumption]
2. ((M v H) v C) > A [assumption]
3. ~(M v H) & C [assumption]
4. M v H [?]
5. C [3 &E]
6. (M v H) v C [5 vI]
7. A > F [1 &E]
8. A [2,5 >E]
9. F > D [1 &E]
10. F [7,8 >E]
11. D [9,10 >E]

Thank you - any help would be greatly appreciated.

 

[moxie]

(Solution Attached in PDF)

Hello, the problem you posted here last year was interesting. Although late, I have found a solution (See Attachment for PDF version) consisting of 24 steps.

The key to this whole thing is deriving (M v H). But anyway, you'll notice the use of negation-elimination (~E) to get line 19, which is the bulk of the work. Also tricky is the double use of wedge-elimination (vE, sometimes called or-elimination) in steps 16 and 17. Finally, the contradiction is made obvious by steps 17 and 18 which allowed for the negation-elimination in step 19. Those are the key points.

G'luck,

Christopher Jackson
Institute for Artificial Intelligence
The University of Georgia