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