Second-Order and Higher-Order Logic

First-order logic quantifies over the objects a structure contains. It does not quantify over the properties those objects have, which is why induction has to be stated as a schema with one instance per formula rather than as the single axiom Dedekind wrote: every property holding of zero and closed under successor holds of every number.

Removing that restriction is a small change to the syntax and an enormous change to everything else. This article sets out what is gained, what is lost, and why the question of whether the result is logic at all has never been settled.

The system

The induction axiom becomes $\forall X\,((X0 \wedge \forall n\,(Xn \rightarrow Xsn)) \rightarrow \forall n\,Xn)$, a single sentence. The least upper bound axiom for the reals becomes a single sentence saying every bounded nonempty set of reals has a least upper bound. Both were schemas in the first-order treatment, and the difference is not cosmetic: a schema has one instance per formula, and there are only countably many formulas, so a schema constrains only the countably many definable sets, while the second-order axiom constrains all of them.

Higher-order logic continues the ascent, adding variables for properties of properties and so on up the finite types. Each further order adds expressive power in principle, though in practice second order is where the interesting results are, since the pattern established there repeats.

Two semantics

The syntax is unambiguous and the semantics is not. When a sentence says every property, which properties does the quantifier range over?

Under standard semantics the promised results arrive. Second-order Peano arithmetic is categorical: all its models are isomorphic to the natural numbers, by Dedekind's argument, since the induction axiom applied to the set of standard elements forces every element to be standard. Second-order real analysis is categorical, all models being isomorphic to the real field. The ambiguity that nonstandard models exploited is closed off, because the induction axiom now speaks of the set of standard elements whether or not a formula defines it.

The cost is stated by a theorem.

The failures do not stop at completeness. Compactness fails, since the sentence set consisting of second-order arithmetic together with $c > \bar{n}$ for every numeral is finitely satisfiable and unsatisfiable. The Löwenheim-Skolem theorem fails, since second-order real analysis has only models of the cardinality of the continuum. And the consequence relation is entangled with set theory: the continuum hypothesis is equivalent to a sentence of pure second-order logic, so which second-order sentences are valid depends on questions independent of the axioms of set theory. Nothing about the validity of that sentence can be settled by reasoning in the logic, since the logic has no proof system in which to reason.

Henkin semantics restores everything. Completeness, compactness and Löwenheim-Skolem all hold, because a Henkin model is a first-order structure of a two-sorted signature. What is lost is exactly the categoricity, since a Henkin model of arithmetic whose second-order domain omits the set of standard elements is a nonstandard model satisfying the induction axiom. The two semantics are not variants of a single logic with a shared metatheory; they are different logics that share a syntax.

Comprehension

The bridge between them is an axiom schema.

A Henkin model satisfies the comprehension schema exactly when its second-order domain contains every set definable by a formula with parameters from the model. Standard models satisfy it trivially, having every set. So comprehension is the axiom that forces a Henkin model partway toward a standard one, and how far it gets depends on which formulas are allowed.

That dependence is what makes the schema interesting. Restricting $\varphi$ to formulas without second-order quantifiers gives arithmetical comprehension, a predicative principle that Weyl argued was all analysis needs. Allowing arbitrary $\varphi$ gives the impredicative full schema, the target of Poincaré's and Russell's objections and of the vicious circle principle. Between them lies a graded family of systems, and comparing what each one proves is the subject of the next article.

Next

Comprehension comes in strengths, and a natural experiment presents itself: take the theorems of ordinary mathematics one at a time and find the weakest comprehension principle each requires. The answer, remarkably, is that almost every theorem is equivalent to one of a very small number of systems.