 Second-order logic, SOL, is a very expressive formal language which differs from FOL (one-sorted first-order logic) in the following respects: (1) alphabet, (2) standard and non-standard semantics and (3) overwhelming expressive power with standard semantics. See the entry on  second-order and higher-order logic  as well as the entry on  Church’s type theory.