Misplaced Pages

Counting quantification

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
(Redirected from Counting quantifiers) Mathematical logical term

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 ( y x P y ) ) {\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 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 ( y x P y ) ) {\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}}}

See also

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 OCLC 282402933
Stub icon

This logic-related article is a stub. You can help Misplaced Pages by expanding it.

Categories: