 First-order definition of exactly finitely many witnesses

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.