# On the Decision Problem for Two-variable First-Order Logic

I have a question concerning the model construction of the $\forall \forall \land \forall \exists$ - Scott sentence on page 6 in this paper:

www.cs.rice.edu/~vardi/papers/basl96.ps.gz

Why do we need to include the "court", i.e. the set C of skolem witnesses of all kings, in the universe of the model B? Wouldn't it suffice to take the union of the sets K,D,E,F and to choose an element of D for every skolem witness of a king, which isn't a king itself?

Thank you

-

There is nobody who is a witness of $\beta_i$ for both king $\mathrm k_1$ and king $\mathrm k_2$ simultaneously.
because kings can effectively be treated as constants -- that is, $R(x,\rm k_1)$ can be expressed with only $x$ as a free variable and yet unambiguously speak about $\rm k_1$, so $\forall x.\bigl[\neg \beta_i(\mathrm k_1,x)\lor \neg \beta_i(\mathrm k_2,x)\bigr]$ is FO².
Therefore it is possible that each king may need separate witnesses for each of the $\beta_i$s, and $D$ is not large enough to contain them all at the same time. On the other hand, non-royal citizens cannot afford to be picky about sharing their witnesses with someone else, at least if the "someone else" has the same 1-type as themselves.
We might try to make $D$ large enough to contain a personal witness for each king, but then it seems we'd run into problems closing the loop from $F$ to $D$, because the element of $D$ we'd ordinarly choose as a witness might already have been claimed by a picky king.