Edit. September 8th, 2013. I've added another another section to the question, which should hopefully constrain its scope. Please see below the horizontal line!!
Lets write the statement 'there is at most one $x$ such that $Px$' symbolically as $!xPx,$ and assert the following definition.
$$!xPx \Leftrightarrow \forall xy(Px \wedge Py \rightarrow x=y).$$
Furthermore, lets define the statement 'there exists unique $x$ such that $Px$' symbolically as follows.
$$\exists! x Px \Leftrightarrow \exists xPx \;\wedge\:\, !xPx$$
I don't have a good understanding of why the conjunction $\exists xPx \;\wedge\:\, !xPx$ is useful. I know, for example, that:
It shows up a lot.
The $\exists$ quantifier can be viewed as asserting the existence of $\geq 1$ of a thing, and the $!$ quantifier can be viewed as asserting the existence of $\leq 1$ of a thing. So together, they say that there is precisely one of a thing.
The statement $\forall x\exists! y Q(x,y)$ holds iff there exists a unique function $f$ such that $\forall xQ(x,f(x))$.
But still, I don't really understand how uniqueness and existence 'work' together. Clearly there's some sort of synergy going on here. The whole is greater than the sum of the parts, kind of thing.
Why does it make sense to pair existence and uniqueness?
Edit. I noticed that, in the presence of the assumption that $Px$ holds for a unique $x$, we have that
$$\forall x(Px \rightarrow Qx) \iff\exists x(Px \wedge Qx)$$
So it makes sense to create the notation $\exists! x(Px \mid Qx)$ to mean: "There exists unique $x$ such that $Px$, and for the unique such $x$ we have $Qx$." In light of the above observation, this can be defined by either of the following formulae.
$\exists! x Px \wedge \forall x(Px \rightarrow Qx)$
$\exists ! x Px \wedge \exists x(Px \wedge Qx)$
Lets also create the notation $\exists x(Px \mid Qx)$ as shorthand for "There exists (not necessarily unique) $x$ such that $Px$, and for all such $x$ we have $Qx$." Symbolically, this can be defined as in a similar way to 1, except without the uniqueness requirement. Namely:
- $\exists x Px \wedge \forall x(Px \rightarrow Qx).$
Now its clear that the following implications hold.
$$\exists ! x (Px \mid Qx) \implies \exists x(Px \mid Qx) \implies \exists x(Px \wedge Qx)$$
My question is this:
Does $\exists ! x (Px \mid Qx)$ have better properties than $\exists x (Px \mid Qx),$ that make it more mathematically useful? If so, what are they?
Note that you need not create an "at most one" quantifier, since as you note, $$\forall x \forall y\Big((P(x) \land P(y)) \rightarrow x = y\Big)$$ states the same: there is at most one "thing" in the universe, let's just call it x, for which P(x) holds. It claims nothing about whether or not P(x) it holds for any "x" in the universe, so it tells us nothing about the existence of anything unique. It tells us that if there is anything such that P is true of that thing, there is at most one such thing.
To make the stronger assertion of existence and uniqueness, then, we simply add the assertion of existence, rearrange quantifiers, giving us: $$\exists x\Big(P(x) \land \forall y(P(y) \rightarrow x = y)\Big)$$