Editing Second-order logic (section)

{{Short description|Form of logic that allows quantification over predicates}}
In [[logic]] and [[mathematics]], '''second-order logic''' is an extension of [[first-order logic]], which itself is an extension of [[Propositional calculus|propositional logic]].{{efn|{{harvtxt|Shapiro|2000}} and {{harvtxt|Hinman|2005}} give complete introductions to the subject, with full definitions.}} Second-order logic is in turn extended by [[higher-order logic]] and [[type theory]].

First-order logic [[Quantifier (logic)|quantifies]] only variables that range over individuals (elements of the [[domain of discourse]]); second-order logic, in addition, quantifies over [[Finitary relation|relations]]. For example, the second-order [[Sentence (mathematical logic)|sentence]] <math>\forall P\,\forall x (Px \lor \neg Px)</math> says that for every [[well-formed formula|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 [[set (mathematics)|set]]s, [[function (mathematics)|function]]s, and other variables (see 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.