I know I have to use the existential elimination rule twice but I'm still having troubles.
∃x∀y((Kyf ↔ x = y) ∧ Bx), ∃x(Kxf ∧ ¬Bx) ⊢ Fa ∧ ¬Fa
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this communityI know I have to use the existential elimination rule twice but I'm still having troubles.
∃x∀y((Kyf ↔ x = y) ∧ Bx), ∃x(Kxf ∧ ¬Bx) ⊢ Fa ∧ ¬Fa
{1} 1. Ǝx[∀y[(Kyf ↔ x=y) & Bx]] Prem. {2} 2. Ǝx[Kxf & ~Bx] Prem. {3} 3. Kbf & ~Bb Assum. TD(b) {4} 4. ∀y[(Kyf ↔ c=y) & Bc] Assum. TD(c) {4} 5. (Kbf ↔ c=b) & Bc 4 UI {3} 6. Kbf 3 &E {4} 7. Kbf ↔ c=b 5 &E {4} 8. (Kbf → c=b) & (c=b → Kbf) 7 ↔E {4} 9. Kbf → c=b 8 &E {3,4} 10. c=b 6,9 MP {4} 11. Bc 5 &E {3} 12. ~Bb 3 &E {3,4} 13. ~Bc 10,12 =E {14} 14. ~(Fa & ~Fa) Assum {4,14} 15. Bc & ~(Fa & ~Fa) 11,15 &I {4,14} 16. Bc 15 &E {4} 17. ~(Fa & ~Fa) → Bc 14,16 CP {3,4} 18. ~~(Fa & ~Fa) 13,17 MT {3,4} 19. Fa & ~Fa 18 DNE {1,3} 20. Fa & ~Fa 1,4,19 EE {1,2} 21. Fa & ~Fa 2,3,20 EE
Here is a proof that uses explosion and a Fitch-style presentation.
The proof checker and description of inference rules can be found in the references below.
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019.