Higher-order logic

Higher-order logic is a family of formal systems that allows quantification over predicates, functions, or other entities beyond individual objects. Its expressive power comes with choices about semantics and proof systems.

First-order logic: A formal logic whose quantifiers range over individual objects, not predicates or relations. It provides the baseline that higher-order quantifiers extend.
Simple type theory: A typed formal system in which functions and predicates are assigned types built from simpler types. It provides a standard typed architecture for higher-order quantification.
Second-order logic: A logic that permits quantification over predicates, relations, or sets of individuals in addition to individuals. It is the most familiar level in the hierarchy of higher-order logics.
HOL Light: A proof assistant based on classical higher-order logic and implemented in a small trusted core. It demonstrates higher-order logic as a practical foundation for machine-checked mathematics.
Predicate logic: A formal system that represents properties and relations with predicates and uses quantifiers to express generality. Higher-order logic extends predicate logic by allowing predicates themselves to be quantified.
Full semantics: An interpretation of higher-order logic in which variables range over all entities of their assigned types. It gives higher-order quantifiers their unrestricted intended ranges.
Monadic second-order logic: A second-order logic in which quantified predicate variables are restricted to unary predicates. It shows how restricting higher-order variables can yield tractable, specialized systems.
Isabelle (proof assistant): A generic theorem prover whose Isabelle/HOL instance supports higher-order logic. Its HOL environment uses higher-order reasoning to formalize mathematics and software properties.
Type theory: A family of formal systems that classifies expressions by types and governs how they may be combined. Typed formulations assign distinct types to objects, predicates, and functions.
Henkin semantics: A semantics for higher-order logic that allows variables to range over selected domains of higher-type entities. It contrasts with full semantics and supports completeness for standard proof systems.

Linked from 5 pages