Negation of Uniqueness Quantifier Is there a negation of uniqueness quantifier? I need to negate an expression which includes a uniqueness quantifier.

Let $\rm A \oplus B$ denote exclusive disjunction (it can be represented as $\rm\neg(A\iff B)$ if desired), and note three facts about unique existence and negated quantification:


*

*$\;\;\;\rm\exists!\, x:Q(x) \iff \exists x:\forall y\;(\neg Q(y) \oplus x=y)$ 

*$\rm\neg \exists x:R(x) \iff \forall x:\neg R(x)$

*$\;\rm \neg \forall x:S(x)\iff\exists x:\neg S(x) $


Putting this all together:
$$\rm \neg\exists!\, x: P(x) \iff \neg(\exists x:\forall y\;(\neg P(y) \oplus x=y))$$
$$\qquad\qquad\quad\rm\iff \forall x\;\neg \forall y (\neg P(y)\oplus x=y)$$ $$\qquad\qquad\qquad\;\rm\iff \forall x\; \exists y:\neg(\neg P(y)\oplus x=y)$$
$$\qquad\qquad\qquad\quad\;\;\iff \forall x \; \exists y:(\neg P(y)\iff  x=y)$$
Alternatively, one can write $\rm P(y)\iff x\ne y$ inside the parentheses.
