Counting quantification

{{Short description|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 <math>\exists_{= k}</math> denote "there exist exactly <math>k</math>". Then :<math>\begin{align} \exists_{= 0} x P x &\leftrightarrow \neg \exists x P x \\ \exists_{= k+1} x P x &\leftrightarrow \exists x (P x \land \exists_{= k} y (P y \land y \neq x)) \end{align}</math> Let <math>\exists_{\geq k}</math> denote "there exist at least <math>k</math>". Then :<math>\begin{align} \exists_{\geq 0} x P x &\leftrightarrow \top \\ \exists_{\geq k+1} x P x &\leftrightarrow \exists x (P x \land \exists_{\geq k} y (P y \land y \neq x)) \end{align}</math>

== 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. [http://www-mgi.informatik.rwth-aachen.de/Publications/pub/graedel/gorc2.ps Postscript file] {{oclc|282402933}}

Category:Quantifier (logic)

{{logic-stub}}