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

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?

• Typically $\exists !$ means "there exists one and only one". But it is possible, that due to the widespread use of ! as NOT in many programming languages, the author(s) chose/choose to use $\exists^{=1}$ instead, to express the more standard $\exists !$. Jun 30 '20 at 12:25
• Jun 30 '20 at 12:46
• @amWhy I like the extra explanation why they might deviate from the standard notation. That comment should be an answer :) Jun 30 '20 at 13:09

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^{ 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 ik}x\:\phi(x)&\iff\exists^{\ge k+1}x\:\phi(x),\\ \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.