language proof and logic chapter 13 question 49 Help

Question

Premises:
∃xP(x) 
∀x∀y((P(x)∧P(y)) → x = y) 
Prove:
∃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.

Answer 1

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.

Answer 2

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.

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.

---

Reference

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/