= First-order definition of exactly finitely many witnesses
{title2=$\exists x_1\cdots\exists x_k\,[\bigwedge_{i<j}x_i\ne x_j\land\bigwedge_iR(x_i)\land\forall y(R(y)\to\bigvee_i y=x_i)]$}
For a fixed positive <integer> $k$, the displayed <first-order logic> sentence says that exactly $k$ distinct elements satisfy $R$. The pairwise inequalities and positive instances give at least $k$ witnesses; the universal exhaustiveness clause gives at most $k$. Additional parameters can remain fixed inside $R$. For $k=0$, use $\forall y\,\neg R(y)$ instead. Omitting distinctness or exhaustiveness changes exactly to a weaker counting condition.
Back to article page
