Higher-Order Logic

Higher-order logic (HOL) is a logic that extends first-order logic by allowing quantification over functions, predicates, and relations. In first-order logic, you can say 'for all x, P(x) holds.' In higher-order logic, you can say 'for all properties P, Q(P) holds' — quantifying not over individuals but over the properties themselves. This additional expressiveness makes HOL capable of formalizing almost all of mathematics, including set theory, arithmetic, and the foundations of analysis, without requiring the complex axiomatic machinery that first-order logic needs to achieve the same coverage.\n\nThe simplest and most widely used form of higher-order logic is Church's simple theory of types, which adds a type system to prevent the paradoxes that plague naive set theory. Every term has a type, and functions can only be applied to arguments of the correct type. This discipline prevents self-referential constructions that lead to contradictions, making the logic consistent relative to standard set-theoretic foundations.\n\nHigher-order logic is the foundation of several major proof assistants, including Isabelle (in its HOL variant), HOL Light, and HOL4. The PVS system is also based on a classical higher-order logic, though with a richer type system. These systems share a common design philosophy: they use classical logic (not constructive), they accept the law of excluded middle and the axiom of choice as primitives, and they model mathematical reasoning in a style that mathematicians already use. The cost of this familiarity is that proofs in HOL do not carry computational content: a proof of existence does not construct a witness.\n\nThe relationship between higher-order logic and Type Theory is one of the great conceptual convergences in formal methods. Church's simple theory of types and the simply-typed lambda calculus are essentially the same system, viewed through different lenses. The Curry-Howard Correspondence extends this connection: in a proof assistant based on type theory, propositions are types and proofs are programs. In a proof assistant based on HOL, propositions are booleans and proofs are derivations. The two approaches are not competitors; they are complementary perspectives on the same underlying structure of mathematical reasoning.\n\nSee also: Logic, Type Theory, Curry-Howard Correspondence, Isabelle, PVS, HOL Light, HOL4, Formal System\n\n\n\n