Questions about higher-order logic, that is logic that allows arbitrary quantification, e.g. over sets of functions.

Logics can be classified by the level of quantification allowed.

  • Zero-order logic allows no quantification; we call this .
  • First-order logic allows quantification over individuals; we often call this predicate logic.
  • Second-order logic allows quantification over sets,

and so on. Higher-order logic is the union of all orders, that is we allow quantification of arbitrary level.

This is necessary, for instance, for accurately specifying properties of (functional) programs with arbitrary types, that is we need higher-order logic for reasoning about higher-order functions.

Questions tagged with this tag should probably also have .

history | excerpt history