counting quantifiers
   HOME

TheInfoList



OR:

A counting quantifier is a
mathematical Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
term for a quantifier of the form "there exists at least ''k'' elements that satisfy property ''X''". In
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
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 In mathematical logic and computer science, two-variable logic is the fragment of first-order logic where formulae can be written using only two different variables. This fragment is usually studied without function symbols. Decidability Some i ...
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 Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics ...
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 In mathematics and logic, the term "uniqueness" refers to the property of being the one and only object satisfying a certain condition. This sort of quantification is known as uniqueness quantification or unique existential quantification, and ...
*
Lindström quantifier In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were ...


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