= Solution
Using <first-order logic> with equality, one suitable sentence is
$$
\boxed{\exists e\,\bigl(Eq(e)\land\exists u\exists v\,[u\ne v\land Sol(e,u)\land Sol(e,v)\land\forall w\,(Sol(e,w)\to(w=u\lor w=v))]\bigr).}
$$
The distinct witnesses give at least two solutions, and the universal clause excludes every third solution. All <variables> are bound, and the same equation variable $e$ is used in every solution predicate. This is an instance of a <first-order definition of exactly finitely many witnesses>.
Back to article page
