Second-Order Logic — Mathematics Knowledge System

Overview

Second-order logic extends first-order logic by allowing quantification not only over individual elements of a domain (∀x, ∃x) but also over predicates, relations, functions, and subsets of the domain (∀P, ∃P). This extra expressive power lets second-order logic pin down structures that first-order logic provably cannot: the second-order induction axiom for arithmetic, 'every set containing 0 and closed under successor contains all natural numbers' (∀P [(P(0) ∧ ∀x(P(x)→P(x+1))) → ∀x P(x)]), categorically characterizes the standard natural numbers up to isomorphism, whereas first-order Peano arithmetic always has nonstandard models by the compactness theorem. This power comes at a steep price, established by Lindström's theorem and related results: second-order logic under its standard (full) semantics has no sound and complete proof system, is not compact, and does not satisfy any analogue of the Löwenheim–Skolem theorem, meaning many of the well-behaved 'finiteness' and proof-theoretic tools of first-order logic simply fail. A widely used compromise is Henkin semantics, in which the second-order quantifiers range only over a specified subset of all possible predicates/relations (rather than literally all of them); under Henkin semantics, second-order logic behaves exactly like a many-sorted first-order logic, regaining compactness and a complete proof system, but losing the categoricity that made full second-order logic attractive in the first place.

Intuition

First-order logic can only say 'for every element x, ...' — it can never directly say 'for every possible subset of the domain, ...' or 'for every possible relation on the domain, ...'; second-order logic lifts that restriction, letting quantifiers range over entire subsets or relations rather than just points. This is exactly what it takes to state real mathematical induction faithfully: first-order Peano arithmetic can only offer an induction schema, one first-order axiom per definable property (infinitely many separate axioms, one for each formula), while the single second-order induction axiom quantifies over ALL subsets at once and thereby rules out every nonstandard model in one stroke. But that same all-subsets quantification is what breaks compactness and completeness — a complete proof system can only ever certify countably many true second-order sentences via finite syntactic derivations, yet 'quantify over all subsets' packs in far too much semantic content (related to the size of the continuum) for any recursively enumerable proof system to keep pace, which is the deep reason full second-order logic has no completeness theorem.

Formal Definition

Definition

Second-order logic adds quantification over predicate/relation/function variables (here P, written as unary for simplicity) to the first-order syntax:

\forall P\, \varphi(P) \quad \text{('for every subset/predicate } P \text{ of the domain, } \varphi(P) \text{ holds')}

Second-order universal quantification over predicates

\forall P\, [(P(0) \wedge \forall x\,(P(x) \rightarrow P(x{+}1))) \rightarrow \forall x\, P(x)]

Second-order induction axiom (categorical for ℕ)

\text{full semantics: } P \text{ ranges over } \mathcal{P}(D) \text{ entirely} \qquad \text{Henkin semantics: } P \text{ ranges over a fixed subset of } \mathcal{P}(D)

Full versus Henkin semantics

\text{(full 2nd-order logic)} \implies \text{no complete proof system, no compactness, no Löwenheim–Skolem}

Cost of full semantics

Worked Examples

The claim quantifies over every possible subset P of the domain, not just definable ones — this quantification over subsets is what makes the sentence second-order.
$\forall P\, [\exists x\, P(x) \rightarrow \exists y\, (P(y) \wedge \forall z\, (P(z) \rightarrow y \le z))]$
A first-order theory can only assert this schema-by-schema for each individually definable P, missing subsets that are not first-order definable in the language.
$\text{first-order: only a schema, one instance per definable } P(x)$

Answer: ∀P[∃xP(x) → ∃y(P(y) ∧ ∀z(P(z)→y≤z))], genuinely second-order because P ranges over ALL subsets of the domain, not merely the (countably many) first-order-definable ones.

Practice Problems

Difficulty 5/10

What is the key syntactic difference between first-order and second-order logic?

Difficulty 6/10

Why does full second-order logic fail to have a sound and complete proof system?

Difficulty 8/10

Explain what Henkin semantics changes about second-order logic, and why it restores compactness and completeness.

Quiz

Summary

Second-order logic adds quantification over predicates, relations, and functions (∀P, ∃P), not just individual domain elements.
This extra power buys categoricity — e.g. the single second-order induction axiom pins down ℕ up to isomorphism — but at the cost of compactness, Löwenheim–Skolem, and any sound complete proof system under full semantics.
Henkin semantics restricts second-order quantifiers to a specified sub-collection of subsets, reducing second-order logic to a well-behaved many-sorted first-order logic, regaining completeness and compactness while losing categoricity.

References

WebsiteWikipedia — Second-order logic