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.
0
2
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.
1
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/
