 Obviously, SOL with general semantics is less expressive than with standard semantics. For instance, \(\forall X(Xx\leftrightarrow Xy)\) is no longer a definition of genuine identity between individuals. And so we take it as primitive and require equality \(\approx\) to be interpreted as identity. For higher types, Axiom of Extensionality