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?

  • $\begingroup$ You can't have $P(y)\wedge \neg P(y')\wedge (y'=y)$. The proposition, as written, is saying exactly what you said in the second to last sentence. $\endgroup$
    – user550929
    Apr 11, 2018 at 11:20
  • $\begingroup$ Because by axiom for equality: if $P(y)$ and $y=y'$, then $P(y')$ follows. $\endgroup$ Apr 11, 2018 at 11:26
  • $\begingroup$ So it is indeed possible to define uniqueness like $\exists x \forall y : P(x) \land P(y) \Leftarrow \Rightarrow x = y$? $\endgroup$
    – Zazaeil
    Apr 11, 2018 at 11:30

2 Answers 2


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))$$


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


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.