Negation of uniqueness quantification in first-order logic I need to make the denial of the following logical expression, but it complicates the unique existence quantifier.
$$\exists !\; n \in \mathbb{N}, \forall \; m\in \mathbb{N} ; (m\cdot n)=m$$
Any contribution works.
 A: The negation is: there exist 2 (different) elements that hold the property or there is none element holding the property, that is:
$$\big(\exists n_1,n_2\in\mathbb{N},n_1\neq n_2,\forall m\in\mathbb{N}: (m\cdot n_1)=m,\; (m\cdot n_2)=m\Big)\vee\big(\forall n\in\mathbb{N},\exists m\in\mathbb{N}: (m\cdot n)\neq m)\Big)$$
A: $$\exists !\; n \in \mathbb{N}, \forall \; m\in \mathbb{N} ; (m\cdot n)=m$$ is equivalent to
$$\exists \; n \in \mathbb{N},[ \forall \; m\in \mathbb{N} ; (m\cdot n)=m \; \wedge \neg\; \exists \;n'\in \mathbb{N}(\forall \; m\in \mathbb{N} ; (m\cdot n')=m \wedge n\neq n') ]$$
which is the same as
$$\exists \; n \in \mathbb{N},[ \forall \; m\in \mathbb{N} ; (m\cdot n)=m \; \wedge \forall \; n'\in \mathbb{N}(\forall \; m\in \mathbb{N} ; (m\cdot n')=m\implies n=n')]$$
equivalently
$$\exists \; n \in \mathbb{N} \; \forall\; n'  \in \mathbb{N}[\forall \; m\in \mathbb{N} ; (m\cdot n')=m\iff n=n']\tag {*}$$
Now if we negate this$(*)$, we get
$$ \forall\; n \in \mathbb{N} \;\; \exists\; n'\in \mathbb{N} \;[\forall \; m\in \mathbb{N} ; (m\cdot n')=m\iff n\neq n']$$
A: Similar to Leyla's answer, but using a somewhat less confusing notation IMHO.
$\exists !\; n \in \mathbb{N}, \forall \; m\in \mathbb{N} ; (m\cdot n)=m$
is equivalent to:
$\exists n:[n\in \mathbb{N} \land \forall m:[m \in \mathbb{N} \implies m\cdot n=m]$
$\land \forall n':[n'\in \mathbb{N} \implies [\forall m:[m\in \mathbb{N}\implies m\cdot n' = m] \implies n'=n]]]$
The negation is:
$\forall n: [n\in \mathbb{N}\land \forall m:[m\in \mathbb{N} \implies m\cdot n=m]$
$\implies\exists n':[n'\in \mathbb{N}\land [\forall m:[m\in \mathbb{N} \implies m\cdot n'=m] \land n'\neq n]]]$
