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.
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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.