SecondOrderLogic

First-order logic quantifies over the things a structure is made of. Second-order logic quantifies over the ways those things can be collected and related: not only “every number has a successor”, but “every property that holds of zero and passes to successors holds of every number”.

That extra reach has a price. The step from one order to the next is not a matter of adding notation: it changes which structures a set of statements can pin down, and it gives up the completeness first-order logic enjoys, since no proof system can capture every second-order consequence.