first order logic - Fitch Formal Proof Question

33 Views Asked by At

I'm doing this by myself over the summer and I'm really confused about construct formal proof with Fitch. Currently stucked on a problem that is asking me to derive Dodec(f) from Dodec(e), ¬Small(e), and ¬Dodec(e) ∨ Dodec(f) ∨ Small(e). I have a partially constructed proof already. Please help me check my steps and let me know how can I conclude it. my proof

Edit: Because some lovely person commeneted on how the picture might not be viewable, here is a text version of my proof

  1. Dodec(e)
  2. ¬Small(e)
  3. ¬Dodec(e) ∨ Dodec(f) ∨ Small(e)
  4. -subproof ¬Dodec(e)
  5. ⊥ (Intro ⊥ 1, 4) - end subproof
  6. ¬¬Dodec(e) (¬ Intro 4-5)
  7. -subproof Dodec(f)
  8. Dodec(f) (Reit 7) - end subproof
  9. -subproof Small(e)
  10. ¬Small(e) (Reit 2)
  11. ⊥ (⊥ Intro 9, 10) - end subproof
  12. Dodec(f) (∨ Elim 3, 7-8, 9-11, 4-5)

Thank you guys so so much!!!