Counting quantification

Counting quantifiers can be defined recursively in terms of ordinary quantifiers.

Let ${\displaystyle \exists _{=k}}$ denote "there exist exactly ${\displaystyle k}$". Then

${\displaystyle {\begin{aligned}\exists _{=0}xPx&\leftrightarrow \neg \exists xPx\\\exists _{=k+1}xPx&\leftrightarrow \exists x(Px\land \exists _{=k}y(Py\land y\neq x))\end{aligned}}}$

Let ${\displaystyle \exists _{\geq k}}$ denote "there exist at least ${\displaystyle k}$". Then

${\displaystyle {\begin{aligned}\exists _{\geq 0}xPx&\leftrightarrow \top \\\exists _{\geq k+1}xPx&\leftrightarrow \exists x(Px\land \exists _{\geq k}y(Py\land y\neq x))\end{aligned}}}$

• Uniqueness quantification
• Lindström quantifier
• Spectrum of a sentence