Exists infinitely many as a numerical-quantifier On notation, at first I just write $\exists^{!\infty}$, later I changed to $\exists^\infty$, which one should I use $?$
And I'm thinking what does this really mean in first-order-logic$\dots$
My attempts (first formalize at least, at most, exact)
$\text{Let n $\in\mathbb{N}$, then }\exists^{\ge n}x,p(x) \text{ if and only if :}$
$$\exists x_1\dots x_n \text{ s.t.}\underbrace{(p(x_1)\wedge\dots\wedge p(x_n))}_{\text{$x_1\dots x_n$ satisfy $p$}}
\wedge\underbrace{(x_1\neq x_2\land\dots\land x_1\neq x_n)\wedge\dots\wedge(x_{n-1}\neq x_n)}_{\text{$x_1\dots x_n$ are distinct}}$$
$$\Leftrightarrow\underset{i=1}{\overset{n}{\exists}} x_i,(\bigwedge_{i=1}^np(x_i))\wedge(\bigwedge_{i=1}^{n-1}(\bigwedge_{j=i+1}^nx_i\neq x_j))$$
$\exists^{\le n}x,p(x) \text{ if and only if :}$
$$\exists^{<n+1}x,p(x)$$
$$\Leftrightarrow\neg(\exists^{\ge n+1}x,p(x))$$
$$\Leftrightarrow \underset{i=1}{\overset{n+1}{\forall}}x_i,(\bigvee_{i=1}^{n+1}\neg p(x_i))\vee(\bigvee_{i=1}^n(\bigvee_{j=i+1}^{n+1}x_i=x_j))$$
$\exists^{!n}x,p(x) \text{ if and only if :}$
$$\exists^{\ge n}x,p(x)\wedge\exists^{\le n}x,p(x)$$
$$\Leftrightarrow\exists^{\ge n}x,p(x)\wedge\neg(\exists^{\ge n+1}x,p(x))$$
$$\Leftrightarrow \underset{i=1}{\overset{n}{\exists}}x_i\forall x_{n+1}(p(x_{n+1})\leftrightarrow(\bigvee_{i=1}^nx_i=x_{n+1}))\wedge\bigwedge_{i=1}^{n-1}(\bigwedge_{j=i+1}^nx_i\neq x_j)$$

The idea is first we define at least $n$, then we notice that at most $n$ is just not (at least $n+1$), also notice exactly $n$ is just at least $n$ and at most $n$.

Then, to express exists infinitely many we can write
$\exists^{\infty}x,p(x)$ if and only if: $$\forall n\in\mathbb{N},\exists^{\ge n}x,p(x)$$
$$\Leftrightarrow \forall n\in\mathbb{N},\underset{i=1}{\overset{n}{\exists}} x_i,(\bigwedge_{i=1}^np(x_i))\wedge(\bigwedge_{i=1}^{n-1}(\bigwedge_{j=i+1}^nx_i\neq x_j))$$
And by taking negation, exists finitely many can be expressed as
$\exists^{<\infty} x, p(x)$ if and only if:
$$\exists n\in\mathbb{N},s.t.\exists^{\le n-1},p(x)$$
$$\Leftrightarrow \exists n\in\mathbb{N},s.t.\underset{i=1}{\overset{n}{\forall}}x_i,(\bigvee_{i=1}^{n} \neg p(x_i))\vee(\bigvee_{i=1}^{n-1}(\bigvee_{j=i+1}^{n}x_i=x_j))$$
Is this correct, any suggestion would be appreciated.
 A: The standard notation in logic would be $\exists^\infty$. 
The exclamation mark ! is used to indicate uniqueness, $\exists^{!n} x\,\phi(x)$ being "there are exactly $n$ distinct elements $x$ such that $\phi(x)$". So, the standard reading of $\exists^{!\infty}x\,\phi(x)$ would be "there are exactly infinitely many $x$ such that..." which is awkward, as it is not very exact to simply say "infinitely many", since there are many options here. And if you are in a setting where the universe of discourse is countably infinite, for instance, then the "exactly" part is superfluous anyway.
You are correct that $\exists^{\infty}x\,\phi(x)$ is the same as $\forall n\,\exists^{\ge n}x\,\phi(x)$. This is the case regardless of whether you are in a situation where the axiom of choice holds. I mention this because using choice, $\exists^{\infty}x\,\phi(x)$ is equivalent to $Q_{\aleph_0}x\,\phi(x)$, where $\aleph_0=|\mathbb N|$ and, for a cardinal $\kappa$, $Q_\kappa x\,\phi(x)$ means that there are at least $\kappa$ distinct values of $x$ such that ... (The $Q_\kappa$ are called cardinality quantifiers in the literature.) However, if choice fails, a set may be infinite without containing a countably infinite subset. 
(And just to avoid confusion, let me add the remark mentioned in comments: Although each $\exists^{\ge n}$ is first-order definable as shown in the question, $\exists^\infty$ is a genuinely new quantifier, meaning that it is not first-order definable by a formula. Otherwise, its negation ("there are only finitely many") would also be first-order definable, and an easy compactness argument gives us a contradiction: the theory $$\{\lnot\exists^\infty x\,(x=x)\land\exists^{\ge n}x\,(x=x)\mid n\in\mathbb N\}$$ is inconsistent but any finite subset is consistent.) 
A: The more words rather than symbols the better for your reader. I suggest 

The proposition $p(x)$ is (or is not) true for infinitely many $x$.

A: I think it will be more clear if you use just standard notation. Instead of say "exists infinitely many $x$ such that $p(x)$" you can say that "there exists $A\subset \Bbb R $ with $|A|\geqslant \aleph _0$ such that for all $x\in A$ then $p(x)$".
You can change $\Bbb R$ by any appropriate set in your context.
In formulas something like
$$
\exists A\forall x\big(|A|\geqslant \aleph _0\land (x\in A\implies p(x))\big)
$$
EDIT:  my answer above try to fit to the case that you want to use standard logic notation to represent what you want, however as said in the answer of @EthanBolker words are better than symbols.
