Second-Order and Higher-Order Logic

First-order logic quantifies only over individuals — the elements of a structure's domain. Second-order logic (SOL) extends it by also quantifying over relations and functions on the domain; higher-order logic (HOL) iterates this, quantifying over relations of relations, functions of functions, and so on up a type hierarchy. The extra expressive power lets these systems pin down structures that first-order logic cannot — but at the cost of the very metatheorems (completeness, compactness) that make first-order logic so well-behaved.

This page assumes the syntax and semantics of first-order logic and focuses on what changes when quantification is allowed over higher types.

Second-order syntax

A second-order language has all the apparatus of first-order logic — constants, function symbols, relation symbols, individual variables $x, y, z, \dots$ — together with two new families of variables:

relation variables $X, Y, Z, \dots$ , each of some arity $n$ , ranging over $n$ -ary relations on the domain;
function variables $F, G, \dots$ , each of some arity $n$ , ranging over $n$ -ary functions on the domain.

Atomic formulas now include $X (t_{1}, \dots, t_{n})$ , where $X$ is an $n$ -ary relation variable and the $t_{i}$ are terms. Crucially, the quantifiers $\forall$ and $\exists$ may bind the new variables, giving sentences such as

$\forall X (X (c) \land \forall y (X (y) \to X (s (y))) \to \forall y X (y)),$

the second-order induction axiom (every set $X$ containing $c$ and closed under $s$ is all of the domain). No first-order sentence is equivalent to this.

A useful gradation:

Monadic second-order logic (MSO): only unary relation variables (quantification over subsets of the domain). Already strictly stronger than first-order logic, and central to automata theory and the theory of graphs.
Full second-order logic: relation and function variables of all arities.

Higher-order logic and the type hierarchy

Higher-order logic organizes objects into a hierarchy of types. In a common formulation (Church's simple theory of types) one starts with a base type $ι$ of individuals (and often a type $o$ of truth values) and closes under function types $σ \to τ$ :

type $ι$ — individuals;
type $ι \to o$ — properties of individuals (equivalently, sets of individuals) — the second-order layer;
type $(ι \to o) \to o$ — properties of properties of individuals — the third-order layer;
and so on.

$n$ -th order logic permits quantification over objects up to the $n$ -th level of this hierarchy. Second-order logic is the case $n = 2$ ; full higher-order logic allows quantification at every finite type. Church's typed $λ$ -calculus provides the standard term language, and HOL in this sense is the logical basis of interactive theorem provers in the HOL family (HOL4, HOL Light, Isabelle/HOL).

Semantics: standard vs. Henkin

Here the story forks, and the fork is the whole point.

Standard (full) semantics. A relation variable of arity $n$ ranges over all $n$ -ary relations on the domain $M$ — that is, over the full power set $P (M^{n})$ — and function variables over all functions. This is the intended reading, and it is what gives second-order logic its strength.

Henkin (general) semantics. A structure additionally specifies, for each type, a designated collection of relations/functions that the higher-order quantifiers range over — a sub-collection of the full power set, required only to be closed enough to interpret the language (comprehension). Under Henkin semantics the higher-order variables are, in effect, just a new sort of first-order object.

The contrast is decisive:

Under Henkin semantics, higher-order logic is essentially a many-sorted first-order logic. It therefore inherits all the good metatheorems — it has a sound and complete proof system, and compactness and Löwenheim–Skolem hold.
Under standard semantics, the metatheorems fail (see below). The added strength is exactly the loss of first-order tameness.

A typical deductive calculus for second-order logic adds, on top of the first-order rules, comprehension axioms

$\exists X \forall x_{1} \dots \forall x_{n} (X (x_{1}, \dots, x_{n}) \leftrightarrow φ)$

(for each formula $φ$ not containing $X$ free), asserting that every definable relation exists, together with a choice schema for function variables. This calculus is sound and complete for Henkin semantics, not for standard semantics.

What the extra power buys — categoricity

The signature achievement of standard second-order logic is categoricity: it can characterize important infinite structures uniquely up to isomorphism, which first-order logic provably cannot (by Löwenheim–Skolem).

Arithmetic. The second-order Peano axioms — the usual first-order axioms with the induction schema replaced by the single second-order induction axiom — are categorical: all their models are isomorphic to the standard natural numbers $(N, 0, s)$ . There are no nonstandard models.
Analysis. The axioms for a complete ordered field, with completeness expressed by second-order quantification over subsets (every bounded set has a least upper bound), are categorical: their only model up to isomorphism is the real numbers $R$ .
Finiteness, well-ordering, connectedness and many other notions that are not first-order definable become expressible in second-order logic.

The price — failure of the metatheorems

Under standard semantics, full second-order logic loses every convenience of first-order logic:

No complete proof system. By Gödel's incompleteness theorems, the standard-semantics validities of second-order logic are not recursively enumerable — there can be no sound, complete, effective deductive system. (Second-order logic can express true arithmetic categorically, so a complete proof procedure would decide truths that incompleteness forbids.) This is the sharpest contrast with first-order logic, which is complete (Gödel's completeness theorem).
No compactness. There is a set of second-order sentences, every finite subset of which has a model, that has no model overall — e.g. axioms forcing categoricity of $N$ together with sentences asserting "there are at least $n$ individuals beyond the standard ones" for each $n$ .
No Löwenheim–Skolem. Categoricity of $R$ already shows the downward theorem fails: an uncountable structure has no countable elementarily-equivalent model.
Entanglement with set theory. The truth value of some second-order sentences is independent of ZFC. The standard-semantics second-order Continuum Hypothesis is a second-order sentence that is valid iff CH holds — so deciding second-order validity would decide CH. Second-order "logic" thus smuggles in substantive set theory, which Quine summarized as "set theory in sheep's clothing."

Summary

	First-order logic	Second-order (standard)	Second-order (Henkin) / HOL
Quantifies over	individuals	individuals + all relations/functions	individuals + designated relations/functions
Categorical $N$ , $R$	no	yes	no
Sound & complete proof system	yes	no	yes
Compactness	yes	no	yes
Löwenheim–Skolem	yes	no	yes
Validities r.e.	yes (semidecidable)	no	yes

The trade-off is unavoidable: expressive power is bought with metatheoretic tameness. Standard second- and higher-order logic can say what first-order logic cannot — categorically describing the naturals and the reals — but forfeit completeness, compactness, and Löwenheim–Skolem. Henkin semantics recovers all the good behavior precisely by reinterpreting higher-order logic as multi-sorted first-order logic. This is the central reason first-order logic remains the default foundation for mathematics, with higher-order systems reserved for settings — notably mechanized theorem proving — where their expressiveness pays its way.

Keyboard shortcuts