What does $\exists^{=1}$ stands for?

Question

In this paper, they use $\exists^{=1}$, I know that $\exists$ stands for there exists. But what does $\exists^{=1}$ stand for? My guess is "Only one existential quantifier". But can someone confirm it?

Answer 1

For any constant $k\in\mathbb N$, $\exists^{=k}x\,\phi(x)$ is a standard notation for “there exist exactly $k$ elements $x$ such that $\phi(x)$”. Similarly, $\exists^{\ge k}x\,\phi(x)$ denotes “there exist at least $k$ elements $x$ such that $\phi(x)$”, and you can now guess what $\exists^{>k}x\,\phi(x)$, $\exists^{\le k}x\,\phi(x)$, and $\exists^{<k}x\,\phi(x)$ mean.

All of these are already definable in the usual first-order logic, hence they should be seen as abbreviations: for example, $$\begin{align*} \exists^{\ge k}x\:\phi(x)&\iff\exists x_1\,\dots\,\exists x_k\:\Bigl(\bigwedge_{1\le i<j\le k}x_i\ne x_j\land\bigwedge_{i=1}^k\phi(x_i)\Bigr),\\ \exists^{>k}x\:\phi(x)&\iff\exists^{\ge k+1}x\:\phi(x),\\ \exists^{<k}x\:\phi(x)&\iff\neg\exists^{\ge k}x\:\phi(x),\\ \exists^{\le k}x\:\phi(x)&\iff\neg\exists^{>k}x\:\phi(x),\\ \exists^{=k}x\:\phi(x)&\iff\exists^{\ge k}x\:\phi(x)\land\exists^{\le k}x\:\phi(x). \end{align*}$$

Another notation in a similar vein is $\exists^\infty x\,\phi(x)$ for “there exist infinitely many $x$ such that $\phi(x)$”. This is not a priori definable in first-order logic, hence it is only used in more specialized contexts: in particular, in theories of arithmetic, where it stands for $\forall y\,\exists x\,\bigl(x\ge y\land\phi(x)\bigr)$, and in the model theory of theories with elimination of infinity.