# What are notations to express uniqueness in formulae and diagrams?

I am familiar with the notation $\exists\,!$ to express both existence and uniqueness. For example $$\;\;\exists\,!x\!:\!P\,(x)\;\;$$ means "there exists a unique $x$ such that $P\,(x)$ holds", for some predicate $P\,$.

Is there some similarly compact notation to denote only uniqueness (i.e. without simultaneously asserting existence)?

In other words, is there a similarly compact, "easy-to-parse" way to express the assertion "$P\,(x)$ holds for at most one $x$"?*

There is a somewhat analogous question for category-theoretic diagrams. I have seen the convention of using a dashed (or dotted) arrow to indicate the universality of the corresponding morphism (see, for example, Algebra by Mac Lane and Birkhoff). Some authors extend this convention to indicate existence-and-uniqueness (e.g. see Turi's Category Theory Lecture Notes). Hence, I see the dashed arrow as the "diagrammatic cousin" of $\exists\,!\,$. Now, suppose we are making some diagram $\mathcal{D}$ featuring objects $A$ and $B$, say.

Is there some convention to graphically represent the assertion "there is at most one morphism $\alpha$ from $A$ to $B$ [such that diagram $\mathcal{D}$ commutes]"?

Thanks!

*Of course, the immediate guess ("back-forming" from $\exists\,!$) is that the lone $!$ serves this purpose. Thus the assertion above would be expressed with $$!\, x\!:\!P\,(x).$$ I see no immediate problems with using $!$ for this purpose (with the possible exception of cases where the context includes many factorials) but I have never seen such usage, and I would prefer to adopt a notation that has at least some currency, even if it does not complement the $\exists\,!$ form as nicely as $!$ does.

-
Why use a notation, which is likely to be cryptic if it is not standard, when words will be more pleasant to read and more precise in meaning? – lhf Sep 28 '11 at 13:14
Sorry, I beg to differ. At any rate, this is a matter of taste, and I would not like to take the conversation in that direction; for those who prefer to avoid notation, my question is of little interest. – kjo Sep 28 '11 at 13:17
I have not seen hypercompact notation for "there is at most one $x$" in research papers in logic, or indeed anywhere else. – André Nicolas Sep 28 '11 at 14:03
In some programming languages != is used for negation of being equal. Hence you can misfire as saying "there does not exist ...." Besides, you are doing nothing but an overload of the readers temporary mental capacity by writing quite definite concepts by ambiguous notation which can be described by exactly one word. – user13838 Oct 1 '11 at 17:05

The notation $\exists^{=n}_xP(x)$ might be useful for you, that means that there exists exactly $n$ entities $x$ for which $P(x)$ is true.
Using this notation, $\exists^{=1}_xP(x)$ means the same than $\exists!_xP(x)$ and $\exists^{=0}_xP(x)$ would mean that there is no such entity $x$.
Thus, what you are looking for would be $\exists^{\le1}_xP(x)$ which could be defined as $\exists^{\le1}_xP(x) :\Leftrightarrow \exists^{=0}_xP(x) \vee \exists^{=1}_xP(x)$