Higher-order logic

In mathematics, higher-order logic is distinguished from first-order logic in a number of ways.

One of these is the scope of quantifiers; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in which this is permitted.

Another way in which higher-order logic differs from first-order logic is in the constructions allowed in the underlying type theory. A higher-order predicate is a predicate that takes one or more other predicates as arguments. In general, a higher-order predicate of order n takes one or more (n − 1)th-order predicates as arguments, where n > 1.

Higher-order logics are more expressive, but their properties, in particular with respect to model theory, make them less well-behaved for many applications.