∀x∀y((P(x)∧P(y)) → x = y) 
∃x(P(x)∧∀y(P(y) → y = x))

I've started it but the end is starting to get super muddy and not work out and I don't know where I went wrong.

enter image description here


The end shouldn't be muddy. The end is where you begin, then work your way in.

Look at where you start and where you wish to go.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|   :
|   :
|  Ex (P(x) ^ Ay (P(y) -> y=x)     ...

Clearly you have to introduce that existential, and the best candidate is by eliminating the existential premise.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|  |_ [a] P(a)                     Assumption
|  |   :
|  |   :
|  |  P(a) ^ Ay (P(y) -> y=a)      ...
|  |  Ex (P(x) ^ Ay (P(y) -> y=x)) Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Elimination

Now you have a universal to eliminate (twice) and one to introduce; and also a conjunction.

|  Ex P(x)                            Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)       Premise
|  |_ [a] P(a)                        Assumption
|  |  |_ [b]                          Assumption
|  |  |  |_ P(b)                      Assumption
|  |  |  |  Ay ((P(a) ^ P(y)) -> a=y) Universal Elimination
|  |  |  |  (P(a) ^ P(b)) -> a=b      Universal Elimination
|  |  |  |   :
|  |  |  |   :
|  |  |  |  b=a                       ...
|  |  |  P(b) -> b=a                  Conditional Introduction
|  |  Ay (P(y) -> y=a)                Universal Introduction
|  |  P(a) ^ Ay (P(y) -> y=a)         Conjunction Introduction
|  |  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))       Existential Elimination

I'm sure you can complete. I'll add a hint: Equality Introduction says b=b.


The following proof is similar to the one suggested by Graham Kemp. What is different is I am using the first eight lines of the OP's proof, showing the use of a different proof checker and offering a way to understand the identity rules.

enter image description here

In this proof note that a = b on line 8 becomes b = a on line 10. To reach this result I have to introduce an identity on line 9, a = a. I don't need to reference any line to introduce this identity. Having this line gives me a line in which I can make a substitution when I use identity elimination.

Identity elimination is so simple it is easy to miss what is going on. Here is how Frederic Fitch describes it (14.3, page 81):

Suppose the (...a...) is any proposition mentioning a, and that (...b...) is the result of substituting b for a in one or more places in (...a...). According to this rule [of identity elimination], we can then infer (...b...) from (...a...) and [a = b].

In the proof above, the identity that is needed for this rule is on line 8, a = b, and the proposition mentioning a in which we will be substituting b for a is line 9, a = a, the very one we introduced as an identity. Line 9 is now not viewed as an identity, but as a proposition containing a. We only substitute the first a in line 9 leaving the other. This allows us to infer line 10: b = a.


Fitch, F. B., Symbolic Logic: An Introduction, 1952.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

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.