6
$\begingroup$

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?

$\endgroup$
3
  • 5
    $\begingroup$ 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 !$. $\endgroup$
    – amWhy
    Jun 30 '20 at 12:25
  • $\begingroup$ See Generalized Quantifiers $\endgroup$ Jun 30 '20 at 12:46
  • 3
    $\begingroup$ @amWhy I like the extra explanation why they might deviate from the standard notation. That comment should be an answer :) $\endgroup$ Jun 30 '20 at 13:09
6
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.