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(y\neq x\land Py))\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(y\neq x\land Py))\end{aligned}}}$ 

• Uniqueness quantification
• Lindström quantifier

• Erich Graedel, Martin Otto, and Eric Rosen. "Two-Variable Logic with Counting is Decidable." In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau. 1997. Postscript file OCLC 282402933