Английская Википедия: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.

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 (y \neq x \land P y)) \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 (y \neq x \land P y)) \end{align}</math>

See also

• Uniqueness quantification
• Lindström quantifier

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 Шаблон:Oclc