Counting quantification: Difference between revisions

Revision as of 18:33, 22 January 2023

Revision as of 18:35, 22 January 2023

Line 10:

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

:<math>\begin{align}

\exists^{= 0} x FP x &\leftrightarrow \neg \exists x FP x \\

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

\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 FP x &\leftrightarrow \top \\

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

\end{align}</math>