Counting quantification

Template:Short description A counting quantifier is a mathematical term for a quantifier of the form "there exists at least k elements that satisfy property X". In first-order logic with equality, counting quantifiers can be defined in terms of ordinary quantifiers, so in this context they are a notational shorthand. However, they are interesting in the context of logics such as two-variable logic with counting that restrict the number of variables in formulas. Also, generalized counting quantifiers that say "there exists infinitely many" are not expressible using a finite number of formulas in first-order logic.

Definition in terms of ordinary quantifiers

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

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

$\begin{array}{cc}{\mathrm{\exists }}_{=0}xPx& \leftrightarrow \mathrm{\neg }\mathrm{\exists }xPx\\ {\mathrm{\exists }}_{=k+1}xPx& \leftrightarrow \mathrm{\exists }x(Px\wedge {\mathrm{\exists }}_{=k}y(Py\wedge y\ne x))\end{array}$

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

$\begin{array}{cc}{\mathrm{\exists }}_{\ge 0}xPx& \leftrightarrow \mathrm{\top }\\ {\mathrm{\exists }}_{\ge k+1}xPx& \leftrightarrow \mathrm{\exists }x(Px\wedge {\mathrm{\exists }}_{\ge k}y(Py\wedge y\ne x))\end{array}$

See also

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

References

• 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 Template:Oclc