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, quantifies over relations. For example, the second-order sentence ${\displaystyle \forall P\,\forall x(Px\lor \neg Px)}$ says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle). Second-order logic also includes quantification over sets, functions, and other variables (see section 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.

First-order logic can quantify over individuals, but not over properties. That is, we can take an atomic sentence like Cube(b) and obtain a quantified sentence by replacing the name with a variable and attaching a quantifier:

$${\displaystyle \exists x\,\mathrm {Cube} (x)}$$

However, we cannot do the same with the predicate. That is, the following expression:

$${\displaystyle \exists \mathrm {P} \,\mathrm {P} (b)}$$

is not a sentence of first-order logic, but this is a legitimate sentence of second-order logic. Here, P is a predicate variable and is semantically a set of individuals.

As a result, second-order logic has greater expressive power than first-order logic. For example, there is no way in first-order logic to identify the set of all cubes and tetrahedrons. But the existence of this set can be asserted in second-order logic as: