Content deleted Content added
|
|
|
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 P x &\leftrightarrow \neg \exists x P x \\
\exists^exists_{= k+1} x P x &\leftrightarrow \exists x (P x \land \exists^exists_{= k} y (P y \neqland xy \landneq P yx))
\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 P x &\leftrightarrow \top \\
\exists^exists_{\geq k+1} x P x &\leftrightarrow \exists x (P x \land \exists^exists_{\geq k} y (P y \neqland xy \landneq P yx))
\end{align}</math>
|
