Content deleted Content added
Undid revision 976758635 by Miaumee (talk) Per User talk:Miaumee, this is apparently the preferred response to poor editing |
Improve formatting |
||
| (7 intermediate revisions by 5 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 ==
Counting quantifiers can be defined [[recursive definition|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 (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 ==
*[[Uniqueness quantification]]
*[[Lindström quantifier]]
*[[Spectrum of a sentence]]
== References ==
Line 13 ⟶ 30:
[[Category:
{{logic-stub}}
| |||