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 | Rightwards arrow | Function type constructor; also the implication constant of type bool → bool → bool |
| λ | U+03BB | Small letter lambda | Function abstraction |
| ∀ | U+2200 | Universal quantifier | A constant of type (α → bool) → bool, at every type α |
| ∃ | U+2203 | Existential quantifier | A constant of type (α → bool) → bool, at every type α |
| ε | U+03B5 | Small letter epsilon | Hilbert choice; ε(λx.P x) satisfies P if anything does |
| ¬ | U+00AC | Negation | Constant of type bool → bool |
| ∧ | U+2227 | Conjunction | Constant of type bool → bool → bool |
| ∨ | U+2228 | Disjunction | Constant of type bool → bool → bool |
| = | U+003D | Equals sign / Equality | Polymorphic; the sole primitive relation, at every type |
| ≠ | U+2260 | Not equal to | Used in the Boolean axiom true ≠ false |
| : | U+003A | Colon | Type ascription; t : α |
| ⟦ ⟧ | — | Semantic brackets | Denotation of a type or term |
| bool | — | Boolean type | Type of propositions; formulas are terms of this type |
| ind | — | Individual type | Base type, asserted infinite by the axiom of infinity |
| α, β | — | Type variables | Rank-1 polymorphism; schematic, not quantifiable inside a formula |
Metatheory. The dividing result is Henkin's (1950). Under standard semantics, where α → β denotes all functions from ⟦α⟧ to ⟦β⟧, the set of validities is not recursively enumerable, so no sound and complete effective proof system exists; compactness and the Löwenheim–Skolem theorems fail, and the compensation is categoricity — the Peano axioms and the axioms for the reals each have exactly one model up to isomorphism. Under general (Henkin) semantics, where each function type denotes some family closed under comprehension, the same proof system is sound and complete, and compactness and Löwenheim–Skolem return, because Henkin models are in effect many-sorted first-order structures. Both readings are undecidable, since first-order logic embeds. Proof-theoretically, cut elimination holds for simple type theory, proved by Takahashi (1967) and Prawitz (1968). Automation faces a hard barrier: higher-order unification is undecidable at third order (Huet 1973) and already at second order (Goldfarb 1981), though higher-order matching is decidable (Stirling 2009). In the Gordon-style systems, extension by definition and by type definition is conservative, which is what licenses building large developments without reproving consistency.
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. The two semantics cannot both be had. Standard semantics delivers categoricity but no complete proof system, since validity is not recursively enumerable; Henkin semantics delivers completeness but readmits the non-standard models — so the reason for going higher-order, pinning down ℕ and ℝ up to isomorphism, is surrendered exactly when the logic becomes axiomatizable, and what a HOL proof assistant actually proves are the Henkin validities. Automation is bounded in principle, not merely in practice: higher-order unification is undecidable (Huet 1973, Goldfarb 1981), so no complete procedure for higher-order resolution exists. The type discipline is simple, not dependent: types cannot be indexed by terms, there is no quantification over type variables within a formula, and polymorphism is schematic at the meta-level only, so a statement about all types is a schema rather than a theorem. Partial functions must be totalized, since every term of function type denotes. And Hilbert choice makes the logic classical and non-constructive, so no computational content is extractable from proofs.
© 2026 Lingenic LLC