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.^[a] 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.
Cite error: There are <ref group=lower-alpha> tags or {{efn}} templates on this page, but the references will not show without a {{reflist|group=lower-alpha}} template or {{notelist}} template (see the help page).