# Higher-order logic

## Formal system of logic / From Wikipedia, the free encyclopedia

#### Dear Wikiwand AI, let's keep it short by simply answering these key questions:

Can you list the top facts and stats about Higher-order logic?

Summarize this article for a 10 year old

In mathematics and logic, a **higher-order logic** (abbreviated **HOL**) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more expressive, but their 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 the complicated and clumsy *ramified theory of types* specified in the *Principia Mathematica* by Alfred North Whitehead and Bertrand Russell. *Simple types* is sometimes also meant to exclude polymorphic and dependent types.^{[1]}