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\dots 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.