Editing Higher-order logic (section)

{{Short description|Formal system of logic}}
In [[mathematics]] and [[logic]], a '''higher-order logic''' (abbreviated '''HOL''') is a form of logic that is distinguished from [[first-order logic]] by additional [[Quantification (logic)|quantifiers]] and, sometimes, stronger [[semantics of logic|semantics]]. Higher-order logics with their standard semantics are more expressive, but their [[Model theory|model-theoretic]] properties are less well-behaved than those of first-order logic.

The term "higher-order logic" is commonly used to mean '''higher-order simple predicate logic'''. Here "simple" indicates that the underlying [[type theory]] is the ''theory of simple types'', also called the ''simple theory of types''. [[Leon Chwistek]] and [[Frank P. Ramsey]] proposed this as a simplification of ''ramified theory of types'' specified in the ''[[Principia Mathematica]]'' by [[Alfred North Whitehead]] and [[Bertrand Russell]]. ''Simple types'' is sometimes also meant to exclude [[type polymorphism|polymorphic]] and [[dependent type|dependent]] types.<ref>Jacobs, 1999, chapter 5</ref>