Uniqueness quantification definition

Question

My textbook introduces shorthand for "exists unique" qualifier $\exists !y [P(y)]$, where full version is: $$\exists y[P(y) \land \forall y'[P(y') \Rightarrow y' = y]]$$

What I can't get is why $\Rightarrow$, not $\Leftarrow \Rightarrow$ used? Saying $\Rightarrow$ means that $P(y')$ could be false, however $y' = y$ or $P(y')$ holds and yet $y' \not = y$. However, as far as I understand, having unique $y$ means that this and only this $y$ would satisfy statement $P$; hence, whenver statement is true, it must be $y$ and vice versa: whenever it is $y$, statement must be true.

Am I missing something?

Answer 1

You don't need the biconditional in the statement

$$\exists y (P(y) \land \forall x (P(x) \rightarrow x=y))$$

because it is already making it explicit that $y$ has property $P$ by the very $P(y)$

But if we are not using $P(y)$, then we can use a binconditional to make sure $y$ has property $P$:

$$\exists y \forall x (P(x) \leftrightarrow x=y)$$

As such, throwing the $P(y)$ back in in statements like

$$\exists y (P(y) \land \forall x(P(x) \leftrightarrow x=y))$$

or

$$\exists y \forall x (P(y) \land (P(x) \leftrightarrow x=y))$$

while still correct, is redundant.

In sum: yes, you thought about this absolutely correctly in that we should try to say that 'all and only those things that are identical to $y$ have property $P$' ... it's just that it can be done without a biconditional, and if you use a biconditional, it can be done a little more efficiently.

Answer 2

We have:

1) $P(y) \land \forall y' \ [P(y') \to y=y']$ --- premise

2) $P(y)$ from 1) by Conjunction elimination

3) $y=y'$ --- assumed [a]

4) $P(y')$ --- from 2) and 3) by Axioms for equality : Substitution

5) $y=y' \to P(y')$ --- from 3) and 4) by Conditional introduction, discharging [a]

6) $P(y') \to y=y'$ --- from 1) by Conjunction elimination and Universal instantiation

7) $P(y') \leftrightarrow y=y'$ --- from 5) and 6) by Biconditional introduction

8) $\forall y' \ (P(y') \leftrightarrow y=y')$ --- from 7) by Universal genaralization

9) $P(y) \land \forall y' \ (y=y' \leftrightarrow P(y'))$ --- from 2) and 8) by Conjunction introduction

10) $\exists y \ [P(y) \land \forall y' \ (y=y' \leftrightarrow P(y'))]$ --- from 9) by Existential introduction.