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

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]$.

• The notation $\exists_n P(x)$ is nice and compact. I have not seen it before. If you are writing a paper in which the idea is often needed, it would be reasonable to use this notation, after defining it. But for most purposes, it is better to use ordinary mathematical English. – André Nicolas Feb 19 '15 at 22:47
• Typo alert - "2" is actually equivalent to $\exists_{n+1}$. – Stephen Montgomery-Smith Feb 19 '15 at 22:55
• @StephenMontgomery-Smith ah! Right! – Conor O'Brien Feb 19 '15 at 23:08

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

• I think the original author probably wants $\geq$ instead of $=$. – Milo Brandt Feb 19 '15 at 23:26

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}

• Clarification: Is $\bigwedge$ similar to $\bigcap$ in the way it goes through all values in an indexed set? – Conor O'Brien Feb 20 '15 at 2:09
• @ConorO'Brien Yes. It's the conjunction of an indexed sequence of terms, similar to the $\sum$ notation of sum of a sequence, and $\prod$ for their product. – Graham Kemp Feb 20 '15 at 2:36