Counting quantification explained

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

\exists ^{=} denote "there exist exactly k ". Then\begin{align} \exists ^{=} x P x &\leftrightarrow \neg \exists x P x \\ \exists ^{=} x P x &\leftrightarrow \exists x (P x \land \exists ^{=} y (y ≠ x \land P y)) \end{align} Let \exists ^{\geq} denote "there exist at least k ". Then\begin{align} \exists ^{\geq} x P x &\leftrightarrow \top \\ \exists ^{\geq} x P x &\leftrightarrow \exists x (P x \land \exists ^{\geq} y (y ≠ x \land P y)) \end{align}

See also

• Uniqueness quantification
• Lindström quantifier

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