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 ∃ = k {\displaystyle \exists _{=k}} denote "there exist exactly k {\displaystyle k} ". Then
∃ = 0 x P x ↔ ¬ ∃ x P x ∃ = k + 1 x P x ↔ ∃ x ( P x ∧ ∃ = k y ( P y ∧ y ≠ x ) ) {\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 ∃ ≥ k {\displaystyle \exists _{\geq k}} denote "there exist at least k {\displaystyle k} ". Then
∃ ≥ 0 x P x ↔ ⊤ ∃ ≥ k + 1 x P x ↔ ∃ x ( P x ∧ ∃ ≥ k y ( P y ∧ y ≠ x ) ) {\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}}}See also
- 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