Counting quantification: Difference between revisions

Revision as of 04:58, 12 November 2022

Latest revision as of 01:57, 19 January 2025

(4 intermediate revisions by 3 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.

Line 8 ⟶ 9:

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

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

:<math>\begin{align}

\exists^exists_{= 0} x F(P x) &\leftrightarrow \neg \exists x F(P x) \\

\exists^exists_{= k+1} x F(P x) &\leftrightarrow \exists x (F(P x) \land \exists^exists_{= k} y (P y \neqland xy \landneq F(y)x))

\end{align}</math>

Let <math>\exists^exists_{\geq k}</math> denote "there exist at least <math>k</math>". Then

:<math>\begin{align}

\exists^exists_{\geq 0} x F(P x) &\leftrightarrow \top \\

\exists^exists_{\geq k+1} x F(P x) &\leftrightarrow \exists x (F(P x) \land \exists^exists_{\geq k} y (P y \neqland xy \landneq F(y)x))

\end{align}</math>

Line 22 ⟶ 23:

*[[Uniqueness quantification]]

*[[Lindström quantifier]]

*[[Spectrum of a sentence]]

== References ==