I am trying to write a formula that defines the structures with even sized domain.
However, since counting is not possible in First Order Logic (wouldn't want to use aggregate terms here), so I need an additional relation symbol which defines a partition of the domain into two equal-sized parts.
I can do this with a binary relation symbol, and it requires that: every domain element appears exactly once in the relation, and the relation is a bijection, so exactly half of the elements in the universe occur as the first element of a pair and the other half of the elements in the universe as the second element.
Im trying to write this in First Order Logic but I am not really sure how to go about doing it. Any help would be greatly appreciated!
It looks like you want a relation $R$ which is irreflexive and symmetric, but which is also "functional" (it describes a graph of a function).
Irreflexive: $\forall x:{\sim}Rxx$.
Symmetric: $\forall x:Rxy\implies Ryx$.
Functional: $\forall x\exists y:Rxy$
$\forall x,y,z:(Rxy\wedge Rxz)\implies y=z$.
Alternatively you could use a function symbol.