 But since standard second-order logic lacks some of the nice properties of first-order logic  (section 4.1),  one could instead go for a two-sorted first-order logic, in which both individuals and relations between individuals are first-class citizens one can quantify over. We would have variables \(x,\) \(y,\ldots\) of sort \(i\) (individuals), and \(X^{2},\) \(Y^{2},\ldots\) of sort \(r\) (binary relations between individuals). However, it is not enough to label our variables as individuals or binary relations, we need them to perform as second-order variables do.  A three-place predicate symbol relating binary relations and individuals, \(\epsilon_{2} xyX^{2}\), needs to be added so that \(\Asymm(X^{2})\) becomes: