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
2
2
{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
0
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.
