8.1 Introduction to higher-order logic (HOL)

Higher-order logic

Definition and key features

Higher-order logic (HOL) extends first-order logic by allowing quantification not just over individuals, but over predicates, functions, and sets. In first-order logic, you can say "there exists some $x$ such that $P(x)$," where $x$ ranges over objects in the domain. In HOL, you can also say "there exists some property $P$ such that $P(x)$," quantifying over the predicates themselves.

This jump in expressive power lets HOL represent complex mathematical structures that first-order logic simply cannot capture: infinite sets, topological spaces, algebraic structures, and more.

A few key features distinguish HOL from first-order logic:

• Higher-order quantification: Variables can range over functions and predicates, not just individuals. You can write $\forall P\, \forall x\, (P(x) \lor \neg P(x))$, quantifying directly over the predicate $P$.
• Lambda abstraction: HOL lets you construct anonymous functions on the fly using $\lambda$-notation (covered in depth later in this unit).
• Type system: Every term in HOL is assigned a type. This prevents ill-formed expressions and blocks paradoxes like Russell's paradox, where unrestricted set comprehension leads to contradictions.

Syntax and semantics

HOL's syntax is richer than first-order logic because it needs to handle both the type system and lambda abstraction.

Types are built from a set of base types (commonly $\iota$ for individuals and $o$ for truth values) using a function-type constructor. If $\alpha$ and $\beta$ are types, then $\alpha \to \beta$ is the type of functions from $\alpha$ to $\beta$. A unary predicate over individuals, for instance, has type $\iota \to o$.

Lambda abstraction lets you form functions directly within the logic. The expression $\lambda x.\, x + 1$ denotes the function that takes $x$ and returns $x + 1$. Functions are first-class objects in HOL: they can be passed as arguments, returned as values, and quantified over.

Semantics are built on a hierarchy of types. At the base level sit individuals. Higher levels contain sets of individuals, functions on those sets, sets of functions, and so on. The standard semantics (sometimes called Henkin semantics in its general form, or full or standard semantics when every possible function at each type is included) interpret each type as a domain, and formulas are evaluated relative to these layered domains.

First-order vs. higher-order logic

Quantification and expressiveness

The core difference: first-order logic quantifies only over individuals in the domain, while HOL quantifies over predicates, functions, and sets as well.

This matters because certain concepts are simply not expressible in first-order logic:

• Finitude and infinity: You cannot write a single first-order sentence that says "the domain is finite." In HOL, you can define finiteness by quantifying over properties of sets.
• Completeness of the reals: The least upper bound property of $\mathbb{R}$ requires quantifying over sets of real numbers, which is inherently second-order.
• Meta-logical properties: Concepts like the consistency or completeness of a formal theory involve statements about all sentences or all proofs, requiring higher-order quantification.

Decidability and completeness

This added expressiveness comes with real trade-offs.

First-order logic enjoys two powerful properties:

• Completeness (Gödel's completeness theorem): every logically valid first-order formula is provable.
• Semi-decidability: there exists an algorithm that will eventually find a proof of any valid first-order formula (though it may run forever on invalid ones). For certain fragments, full decidability holds.

Higher-order logic, under standard (full) semantics, loses both:

• It is incomplete: no proof system can derive all valid HOL formulas. This follows from the fact that HOL with standard semantics can characterize the natural numbers up to isomorphism, so Gödel's incompleteness theorems apply.
• It is undecidable: no algorithm can determine the validity of arbitrary HOL formulas.

Advantages of higher-order logic

Formalization of complex concepts

HOL can directly formalize mathematical structures that require quantification over sets or functions:

• Analysis and topology: Concepts like continuity, compactness, and convergence involve quantifying over sets of points or families of open sets.
• Algebra: Defining what it means to be a group, ring, or field involves quantifying over operations (functions) and their properties.
• Infinite structures: HOL can reason about infinite sets, infinite sequences, and infinite games without the workarounds that first-order logic requires (such as axiom schemas standing in for single higher-order axioms).
• Meta-logic: HOL can express statements about the consistency and completeness of theories, which is central to the study of mathematical foundations.

Applications in computer science

HOL has found significant practical use in computer science, particularly in formal verification:

• Program reasoning: Higher-order functions and predicates map naturally onto programming concepts. A function that takes another function as input (like map or fold) is directly representable in HOL.
• Abstract data types and modules: HOL can specify and reason about interfaces, encapsulation, and object-oriented structures.
• Verified systems: Proof assistants based on HOL (such as Isabelle/HOL and HOL4) have been used to verify real-world systems, including the seL4 microkernel and parts of compilers. These verifications provide mathematical guarantees of correctness.

Intuitive expression of mathematics

HOL aligns more closely with how mathematicians actually write and think. When a mathematician writes "for every continuous function $f$..." they are quantifying over functions, which is a second-order statement. In first-order logic, expressing this requires encoding functions as sets of ordered pairs and adding axioms to ensure they behave like functions. In HOL, you just write it directly.

This directness makes HOL proofs more concise and more readable. The gap between informal mathematical reasoning and formal proof shrinks considerably, which is one reason HOL-based proof assistants have gained traction for large-scale formalization projects.