Counting quantification: Difference between revisions

Revision as of 04:57, 12 November 2022

Revision as of 04:58, 12 November 2022

Line 8:

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^{= 0} x F(x) &\leftrightarrow \neg \exists x F(x) \\

\exists^{= k+1} x F(x) &\leftrightarrow \exists x (F(x) \land \exists^{= k} y (y \neq x \land F(y)))

\end{align}</math>

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

:<math>\begin{align}

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