What are notations to express uniqueness in formulae and diagrams?

Question

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.}

Answer 1

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