I would like to characterize the class of (finite) structures that can be partitioned into two disjoint sets $X,Y$ having the same cardinality, using second order logic (with usual logical connectives plus equality) :
we can define an unary predicate $X(x)$ that is true iif $x \in X$ and a binary predicate $B(x,y)$ for the 1:1 mapping between elements of $X$ and $Y$; so we have:
$\exists X, \exists B$
$(\forall x,y \; B(x,y)\rightarrow B(y,x))$ (B is symmetric)
$\land (\forall x,y,z \; (B(x,y) \land B(x,z))\rightarrow y=z)$ (B is a mapping)
$\land (\forall x \; X(x) \rightarrow \exists y (\neg X(y) \land B(x,y)))$ (every element of X is mapped to an element of Y)
$\land (\forall x \; \neg X(x) \rightarrow \exists y (X(y) \land B(x,y)))$ (every element of Y is mapped to an element of X)
Is there a more succinct formula?