Counting quantification: Difference between revisions

Revision as of 16:35, 30 May 2007

Latest revision as of 01:57, 19 January 2025

(15 intermediate revisions by 13 users not shown)

Line 1:

{{Short description|Mathematical logical term}}

A '''counting quantifier''' is a [[Mathematics|mathematical]] term for a [[Quantifier (logic)|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 ==

==References==

Counting quantifiers can be defined [[recursive definition|recursively]] in terms of ordinary quantifiers.

* 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.

http://www-mgi.informatik.rwth-aachen.de/Publications/pub/graedel/gorc2.ps

Let <math>\exists_{= k}</math> denote "there exist exactly <math>k</math>". Then

[[Category:Quantification]]

:<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 (P y \land y \neq x))

\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 (P y \land y \neq x))

\end{align}</math>

== See also ==

{{Mathlogic-stub}}

*[[Uniqueness quantification]]

*[[Lindström quantifier]]

*[[Spectrum of a sentence]]

== 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. [http://www-mgi.informatik.rwth-aachen.de/Publications/pub/graedel/gorc2.ps Postscript file] {{oclc|282402933}}

[[Category:QuantificationQuantifier (logic)]]

{{Mathlogiclogic-stub}}