Counting Quantifiers

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 \exists^ x F(x) &\leftrightarrow \neg \exists x F(x) \\ \exists^ x F(x) &\leftrightarrow \exists x (F(x) \land \exists^ y (y \neq x \land F(y))) \end$
Let $\exists^$ denote "there exist at least $k$". Then
:$\begin \exists^ x F(x) &\leftrightarrow \top \\ \exists^ x F(x) &\leftrightarrow \exists x (F(x) \land \exists^ y (y \neq x \land F(y))) \end$

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

Quantifier (logic)

{{logic-stub