How can I prove that both of the following definitions of the uniqueness quantifier in first-order logic are equivalent?

Question

First definition:

$$\exists!x:P(x)\iff\exists x(P(x)\wedge\forall y(P(y)\implies y=x))$$

Second definition:

$$\exists!x:P(x)\iff\exists x(P(x)\wedge\forall y\forall z(P(y)\wedge P(z)\implies y=z))$$

I already know that the second definition of uniqueness implies the first one, because if the predicate holds true for all values of $z$, then it also holds true for only the values of $z$ for which $z=x$, which would leave us with a predicate which is equivalent to the first definition. But how do I prove that the first definition of uniqueness also implies the second one?

Answer 1

I already know that the second definition of uniqueness implies the first one, because if the predicate holds true for all values of z, then it also holds true for only the values of z for which z=x, which would leave us with a predicate which is equivalent to the first definition. But how do I prove that the first definition of uniqueness also implies the second one?

It is basically the same reasoning.   Because a universal statement (form of $\forall y~Q(y)$) can be eliminated to arbitrary variables of any letter (ie: not just $y$, but also $z$).

So take arbitrary $y$ and arbitrary $z$ and derive $~P(y)\land P(z) \to y=z~$ by way of $~P(y)\to y=x~$ and $~P(z)\to z=x~$ and equality elimination.

Answer 2

You essentially want the derivation of $$\exists x\;\Big(Px\wedge\forall y\forall z\;\big( Py\wedge Pz \to y=z\big)\Big)$$ from $$\exists x\;\Big(Px\wedge\forall y\;\big(Py\to y=x\big)\Big).$$

Here's one proof, using the proof system at https://proofs.openlogicproject.org/ with additional inference rules Equality Introduction and Substitution:

Answer 3

Using a form of natural deduction (screenshot from my proof checker):

Answer 4

For a start, I think it can be easier to think of your problem in terms of two equivalent formulas about the predicate $P$ instead of two equivalent definitions, that is to consider this equivalence: $$ \exists u (P(u) \land \forall v (P(v) \Rightarrow v = u)) \Leftrightarrow \exists x P(x) \land \forall y \forall z (P(y) \land P(z) \Rightarrow y = z) $$ Note that I changed also the variable names to have them all distinct. It can help avoid confusion during the proof.

$\Rightarrow$ direction

We know that there exists $u$ such that $P(u)$ (1) and $\forall v(P(v) \Rightarrow v = u)$ (2). Now take $x = u$ and we can infer $\exists x P(x)$. Now consider arbitrary $y$ and $z$ such that $P(y)$ and $P(z)$ hold. We can apply (2) to deduce $y = u$ and $z = u$. Using the properties of equality we obtain $y = z$, which completes the proof of the right side.

$\Leftarrow$ direction

We know $\exists x P(x)$ (3) and $\forall y \forall z (P(y) \land P(z) \Rightarrow y = z)$. We can take $x = u$ and infer $P(u)$ from (3). Now consider an arbitrary $v$ such that $P(v)$. We can apply (4) on $y = v$ and $z = u$ to obtain $v = u$ and complete the proof.

Discussion

Notice that if we replace equality with an arbitrary binary predicate $Q$, the $\Leftarrow$ will still work, but the $\Rightarrow$ direction needs $Q(y, u) \land Q(z, u) \Rightarrow Q(y, z)$ for the last step. So in some sense the second definition is stronger because it implies the first one without relying on what equality is as a binary relation.