nLab counting quantifier

Idea

Counting quantifiers generalize existential quantifiers in a logic with a notion of equality.

• $(\exists^{\geq k}x)P(x)$: there exists at least $k$ elements such that $P$ holds,
• $(\exists^{=k}x)P(x)$: there exists exactly $k$ elements such that $P$ holds.

Expressivity

Counting quantifiers increase the expressive power of two-variable logic? while keeping the satisfiability problem decidable.

References

• E. Gradel, M. Otto and E. Rosen, “Two-variable logic with counting is decidable,” Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, 1997, pp. 306-317.

Related concepts

• existential quantifier
• majority quantifier?
• generalized quantifier