nLab counting quantifier

Contents

Contents

Idea

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

  • ( kx)P(x)(\exists^{\geq k}x)P(x): there exists at least kk elements such that PP holds,
  • ( =kx)P(x)(\exists^{=k}x)P(x): there exists exactly kk elements such that PP 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.

Created on June 14, 2024 at 14:19:59. See the history of this page for a list of all contributions to it.