Counting quantification: Difference between revisions

Revision as of 04:58, 12 November 2022

Revision as of 18:33, 22 January 2023

Line 10:

Let <math>\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^{\geq k}</math> denote "there exist at least <math>k</math>". Then

:<math>\begin{align}

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

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

\end{align}</math>