Higher-Order Logic

Origin. Alonzo Church's simple theory of types (1940) combined lambda calculus with logic. Leon Henkin provided semantics (1950). Mike Gordon developed HOL for hardware verification (1980s). Basis for major proof assistants: Isabelle/HOL, HOL4, HOL Light, PVS. Distinct from second-order logic in treatment of types and functions.

Models. Functions and predicates as first-class objects with full comprehension. Quantify over functions of any type. "For all functions f..." is a formula. Combines the expressiveness of higher-order quantification with the computational content of typed lambda calculus. More tractable than second-order logic due to Henkin semantics.

Formalism.

Types:

Base types: bool (propositions), ind (individuals), or domain-specific
Function types: α → β (functions from α to β)
Type variables: α, β, ... (polymorphism)

Examples: ind → bool (predicates), (ind → bool) → bool (second-order predicates), (α → β) → (α → β) (function transformers)

Terms:

Variables: xᵅ (typed)
Constants: cᵅ (typed)
Application: (f t) where f : α → β, t : α
Abstraction: λx.t where x : α, t : β gives λx.t : α → β

Formulas: Terms of type bool. Connectives are constants:

¬ : bool → bool
∧, ∨, → : bool → bool → bool
∀ᵅ, ∃ᵅ : (α → bool) → bool

Axioms (Church/HOL):

Boolean: true ≠ false, cases on bool
Extensionality: (∀x. f x = g x) → f = g
Choice: ε(λx.P x) satisfies P if anything does
Infinity: ind is infinite

Henkin semantics: Types denote sets. α → β denotes some (not necessarily all) functions from ⟦α⟧ to ⟦β⟧. Standard semantics: all functions. Henkin: enough functions to satisfy comprehension. Henkin semantics makes HOL complete; standard semantics does not.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Function type	Type of functions
λ	U+03BB	Lambda	Function abstraction
∀	U+2200	Universal	For all (at any type)
∃	U+2203	Existential	There exists
ε	U+03B5	Choice/Hilbert	Some element satisfying
=	—	Equality	Polymorphic equality
:	—	Has type	Type annotation
bool	—	Boolean	Type of propositions
ind	—	Individual	Base type
α, β	—	Type variables	Polymorphic types

Metatheory. With Henkin semantics: sound and complete, compact. With standard semantics: incomplete (like second-order). Undecidable (subsumes first-order). Henkin models are "enough" for proof — you can prove exactly what's true in all Henkin models. Conservativity: HOL is conservative over Church's type theory. Cut elimination for sequent calculus formulations.

Applies to. Proof assistants (Isabelle/HOL, HOL4, HOL Light). Hardware verification (Gordon's original motivation). Formalized mathematics. Software verification. Semantics of programming languages. Any domain needing higher-order reasoning with automation.

Limitations. More complex than first-order; automation harder. Type system restricts some mathematical constructions (dependent types more flexible). Choice/Hilbert epsilon is non-constructive. Different proof assistants make different foundational choices. The gap between standard and Henkin semantics is philosophically significant. Learning curve for effective use.