Denotation of existence of $n$ distinct $x$ such that $P(x)$?

Question

I have that $\exists!x:P(x)$ means that there exists exactly one $x$ where $P(x)$ holds; this is a more specific version of existential quantification with $\exists$. My problem stands like this.

I have a need to say that there exists not one but $n$ solutions exist to some $P(x)$. As how to denote this, I have a few ideas, but I'm not entirely sure as to what the correct notation actually is:

1. $\exists_nx:P(X)$
2. $\exists x_1,\ldots,x_n:(x_1\neq\cdots\neq x_n )\land(P(x))$
3. $\exists a\in\{x_i\}_{i\in I}(\#\{x_i\}_{i\in I}=n):P(a)$

"2." seems to be the proper way of doing it, but "1." seems more natural; "3." was suggested to me by a friend.

So, what is the correct way of doing it (whether it be one of the above, or somehow else)?

Edit: examples

A trivial example would be $\forall y>0\left[\exists_2x\left(x^2=y\right)\right]$.

Answer 1

I think that $|\{ x: P(x) \}|=n$ is a suitable way to write it down, where $|\cdot |$ denotes the cardinality of a set.

Answer 2

Just as the uniqueness quantifier, $\exists!\;$, provides a way to compactly express "exists exactly one", first order logic can also be extended to express statements like "exists at least five", "exists no more that two", and so forth, by using counting quantification.

You can express these concepts using FOL quantifiers, though it can get a little awkward.   The compact notation is a convenient shorthand.

It appears to me that the most usual convention is to place an order comparator and integer in the superscript after the existential quantifier.

$$\begin{align} \exists^{=1} x\; P(x) \quad&\equiv\quad \exists! x\; P(x) \quad\equiv\quad \exists x\,\forall x' \big(P(x')\leftrightarrow x=x'\big) \\[4ex] \exists^{\geqslant n}x\;P(x) \quad&\equiv\quad \exists x_1\ldots \exists x_n \Big(\bigwedge_{i<j}(x_i\neq x_j) \;\wedge\; \bigwedge_i P(x_i) \Big) \\[4ex] \exists^{=n} x\; P(x) \quad&\equiv\quad \exists x_1\ldots \exists x_n \Big(\bigwedge_{i<j}(x_i\neq x_j) \;\wedge\; \forall x' \big(P(x')\leftrightarrow \bigvee_i (x_i= x')\big) \Big) \end{align}$$