# Counting quantification

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.