2

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

enter image description here

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.