Second-order logic(SOL) is an extension of first-order logic with quantifiers and variables that range over subsets of the universe of discourse, and hence is a higher-order logic of stage 2.

An important fragment is Monadic Second-order logic (MSOL), where second-order quantification is restricted to second-order unary relations between subsets i.e. MSOL quantifies only over set predicates e.g. $\forall X.\varphi(X)$ but not $\forall X\forall Y .\varphi(X,Y)$.

Remark

As SOL permits characterization of mathematical structures up to isomorphism, it is sometimes promoted as a contender to set theory for the foundations of mathematics (cf. references).