Second-order logic

In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.

First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence ${\displaystyle \forall P\,\forall x(x\in P\lor x\notin P)}$ says that for every unary relation (or set) P of individuals, and every individual x, either x is in P or it is not (this is the principle of bivalence). Second-order logic also includes quantification over functions, and other variables as explained in the section Syntax and fragments below. Both first-order and second-order logic use the idea of a domain of discourse (often called simply the "domain" or the "universe"). The domain is a set over which individual elements may be quantified.

The syntax of second-order logic tells which expressions are well formed formulas. In addition to the syntax of first-order logic, second-order logic includes many new sorts (sometimes called types) of variables. These are:

...
Wikipedia