Second-Order Languages

First-order logic quantifies over the members of a structure's universe and nothing else. A quantifier $\forall v_{1}$ ranges over individuals; there is no way to say for every relation or for every function. That restriction is what gives first-order logic its good behavior: compactness, completeness, the Löwenheim–Skolem theorems. Second-order logic lifts the restriction. We add variables that stand for relations and functions and allow quantifiers to bind them, obtaining a language that can single out structures the first-order language cannot even approximate. The metatheorems that made first-order logic tractable fail under the change.¹

The formula

\exists x (P x \to \forall x P x)

is valid — true in every structure, no matter how the predicate parameter $P$ is interpreted. Because its truth does not depend on the reading of $P$ , we are entitled to bind $P$ itself and assert

\forall P \exists x (P x \to \forall x P x),

a sentence whose only parameter is the quantifier symbol. Here $P$ has been promoted from a fixed parameter to a bound predicate variable, and the sentence quantifies over all possible interpretations of a one-place relation.

The additional symbols

To the alphabet of first-order logic we adjoin two new families of logical symbols.

Predicate variables. For each positive integer $n$ , the $n$ -place predicate variables $X_{1}^{n}, X_{2}^{n}, \dots$ , each ranging over $n$ -ary relations on the universe.
Function variables. For each positive integer $n$ , the $n$ -place function variables $F_{1}^{n}, F_{2}^{n}, \dots$ , each ranging over $n$ -ary operations on the universe.

The ordinary variables $v_{1}, v_{2}, \dots$ are now called individual variables to prevent confusion. Subscripts and superscripts are dropped when they are immaterial or clear from context.

Terms are built as before from constant symbols and individual variables by applying function symbols — where function symbols now includes both the function parameters of the language and the new function variables. Atomic formulas are still strings $P t_{1} \dots t_{n}$ in which $P$ is an $n$ -place predicate symbol (a parameter or a variable) and each $t_{i}$ is a term. The inductive definition of well-formed formula gains two clauses.

Predicate parameters and free predicate variables play essentially the same role, mirroring the tight relationship between constant symbols and free individual variables, and between function parameters and free function variables. The genuinely new content is the two quantifier clauses.

Three tiers of variable. Individual variables range over points of the universe; predicate variables over its relations; function variables over its operations. Only the top two tiers are new.

Satisfaction with the new quantifiers

A structure remains what it was for first-order logic: a function on the parameters supplying a nonempty universe and interpreting each predicate, function, and constant symbol. Nothing about the structure changes. What changes is the assignment $s$ and the satisfaction recursion.

Let $V$ be the set of all variables. A variable assignment $s$ now sends each variable to an object of the matching type:

$s (v_{i})$ is a member of the universe $∣ A ∣$ ,
$s (X_{i}^{n})$ is an $n$ -ary relation on $∣ A ∣$ ,
$s (F_{i}^{n})$ is an $n$ -ary operation on $∣ A ∣$ .

The value $s (t)$ of a term is defined by the obvious recursion: if $F$ is a function variable, $s (F t_{1} \dots t_{n})$ applies the operation $s (F)$ to $s (t_{1}), \dots, s (t_{n})$ . Satisfaction of an atomic formula built from a predicate variable $X$ reads off the relation $s (X)$ assigns:

⊨_{A} X t_{1} \dots t_{n} [s] ⟺ ⟨ s (t_{1}), \dots, s (t_{n})⟩ \in s (X) .

The connective and individual-quantifier clauses are unchanged. The two new clauses interpret the second-order quantifiers by ranging over all relations and all functions of the right arity.

The word standard marks the decisive choice: $\forall X^{n}$ quantifies over every relation on the universe — the entire power set of $n$ -tuples — with no room for interpretation. Only the values of $s$ at variables occurring free matter, so a sentence is unambiguously true or false in $A$ , and logical implication $Σ ⊨ σ$ is defined exactly as before. General structures relax this; here the range of a second-order quantifier is fixed to everything on the universe.

A second-order quantifier over a one-place predicate variable ranges over the full power set of the universe, one binding covering every subset at once.

Expressive power of the language

Four properties that no set of first-order sentences can capture each become a single second-order sentence.

Well-ordering. An ordering is a well-ordering when every nonempty subset has a least element. Quantifying over the subset $X$ ,

\forall X (\exists y X y \to \exists y (X y \land \forall z (X z \to y \leq z))) .

The induction postulate. Peano's induction axiom states that any set of natural numbers containing $0$ and closed under successor is all of them. In the second-order language of arithmetic this is one sentence:

\forall X (X 0 \land \forall y (X y \to X S y) \to \forall y X y) .

Least upper bounds. In an ordered field, every bounded nonempty set has a least upper bound:

\forall X [\exists y \forall z (X z \to z \leq y) \land \exists z X z \to \exists y \forall y^{'} (\forall z (X z \to z \leq y^{'}) \leftrightarrow y \leq y^{'})] .

Infinity. A set is infinite exactly when it carries a transitive irreflexive relation whose domain is the whole set, or equivalently when it admits an injection that is not surjective. Either fact is one sentence:

λ_{\infty} : \exists X [\forall u \forall v \forall w (X uv \to X v w \to X u w) \land \forall u \neg X uu \land \forall u \exists v X uv],

\exists F [\forall x \forall y (F x = F y \to x = y) \land \exists z \forall x F x \neq = z] .

Worked example (Infinitude in one sentence). Evaluate $λ_{\infty}$ in a finite structure and in $(N; <)$ .

The sentence claims a relation $X$ that is transitive, irreflexive, and serial — every point has an $X$ -successor, $\forall u \exists v X uv$ . In $(N; <)$ the ordering $<$ witnesses it: $<$ is transitive and irreflexive, and each $n$ has $n < n + 1$ , so

⊨_{(N; <)} λ_{\infty} .

In a finite set $A = {a_{1}, \dots, a_{k}}$ no witness exists. A transitive irreflexive relation is a strict partial order, and a finite strict partial order has a maximal element $a$ — one with no $b$ satisfying $X ab$ . Seriality fails at $a$ , so the third conjunct is false under every choice of $X$ , giving

\neq ⊨_{A} λ_{\infty} .

Hence $λ_{\infty}$ is true in exactly the infinite structures. One sentence captures the class that first-order logic reaches only through the infinite set ${λ_{2}, λ_{3}, \dots}$ .

In first-order logic there are at least $n$ things needs a separate sentence $λ_{n}$ for each $n$ , and infinitude is captured only by the infinite set ${λ_{2}, λ_{3}, \dots}$ — never by a single formula, since compactness forbids it. Second-order logic states the same class of models, the infinite structures, with the one sentence $λ_{\infty}$ .

Comprehension

The second-order language can also assert that relations and functions exist. For any formula $φ$ in which the $n$ -place predicate variable $X^{n}$ does not occur free,

\exists X^{n} \forall v_{1} \dots \forall v_{n} [X^{n} v_{1} \dots v_{n} \leftrightarrow φ]

is valid: it says there is a relation holding of exactly the tuples that satisfy $φ$ . These are the relation comprehension formulas, and there is a matching function comprehension schema asserting that a formula defining a total single-valued relation is the graph of some function. Comprehension records the standard semantics' commitment: every formula-definable relation is actually present in the range of the predicate quantifiers, because that range is the full power set. As the defining axioms of general structures, these comprehension sentences can no longer be taken for granted.

Categoricity

This expressiveness makes structures categorical — determined up to isomorphism by a set of sentences.

First-order logic cannot be categorical for any structure with an infinite model: by the Löwenheim–Skolem theorems an infinite first-order model has models of every larger cardinality, none of them isomorphic to it. Second-order logic escapes this. Take the language with parameters $0$ and $S$ , and the sentences

\forall x S x \neq = 0, \forall x \forall y (S x = S y \to x = y),

together with the second-order induction postulate. Every model is isomorphic to the standard structure $(N; 0, S)$ : the induction axiom rules out the extra $Z$ -chains that a first-order theory of successor must tolerate. The set is categorical.

Second-order induction is categorical for arithmetic. The first-order successor axioms permit an extra integer-like chain disconnected from zero; the induction axiom quantifies over the subset of standard points and forbids it.

Worked example (Categoricity of second-order successor arithmetic). Every model of the two successor axioms together with second-order induction is isomorphic to $(N; 0, S)$ .

Let $A$ satisfy $\forall x S x \neq = 0$ , $\forall x \forall y (S x = S y \to x = y)$ , and the induction postulate. Define $h : N \to ∣ A ∣$ by $h (0) = 0^{A}$ and $h (n + 1) = S^{A} (h (n))$ . Its image

R = {(S^{A})^{n} 0^{A} : n \in N}

is a subset of $∣ A ∣$ containing $0^{A}$ and closed under $S^{A}$ . Because standard induction quantifies over every subset, the induction postulate forces $R = ∣ A ∣$ , so $h$ is onto.

$h$ is one-to-one. By $\forall x S x \neq = 0$ , no $h (k + 1) = S^{A} (h (k))$ equals $h (0) = 0^{A}$ ; and $\forall x \forall y (S x = S y \to x = y)$ gives $h (m + 1) = h (n + 1) \Rightarrow h (m) = h (n)$ , so induction on $min (m, n)$ rules out any clash. Thus $h$ is an isomorphism and $A ≅ (N; 0, S)$ . A general model may omit this very subset $R$ , which is where categoricity later breaks down.

The same construction characterizes other structures. Conjoining the first-order axioms for an ordered field with the second-order least-upper-bound sentence produces a sentence whose models comprise the isomorphs of the ordered field of real numbers and nothing else. Where first-order logic can only characterize classes of structures loosely, second-order logic can name individual structures.

The metatheorems fail

Every metatheorem that made first-order logic well-behaved fails for standard second-order semantics, and the same sentence $λ_{\infty}$ shows why.

The witness is ${\neg λ_{\infty}, λ_{2}, λ_{3}, \dots}$ . Each finite subset mentions only $\neg λ_{\infty}$ and finitely many $λ_{n}$ , so a large enough finite set satisfies it. But the whole set demands a structure that is not infinite yet has at least $n$ elements for every $n$ , which is impossible. First-order compactness depended on exactly the finiteness that $λ_{\infty}$ defeats.

The Löwenheim–Skolem theorems fail too. Call the language with equality and no parameters other than the quantifier the language of equality; a structure for it is just a nonempty set, determined up to isomorphism by its cardinality.

The construction takes the sentence characterizing the real ordered field up to isomorphism, then existentially quantifies over its parameters $0, 1, +, \cdot, <$ — replacing each with a variable of the matching type. The result is true in a bare set precisely when that set can be organized into a copy of the reals, which happens exactly when its cardinality is $2^{ℵ_{0}}$ . No first-order sentence can constrain a set's cardinality this way; downward Löwenheim–Skolem would immediately supply a countable model.

Finally, the enumerability of validity collapses.

The argument reruns Tarski's undefinability theorem: the second-order theory $T^{2}$ of $N$ is not second-order definable in $N$ . Because the categorical sentence $α$ — the arithmetic axioms $A_{E}$ conjoined with second-order induction — has only $N$ as a model,

σ \in T^{2} ⟺ (α \to σ) is valid,

so second-order validity is at least as complex as $T^{2}$ . It is therefore neither arithmetical nor recursively enumerable: the enumerability theorem, and with it any hope of a complete deductive calculus, fails for standard second-order logic.

Property	First-order logic	Standard second-order logic
Compactness	holds	fails
Löwenheim–Skolem	holds	fails (cardinality is definable)
Completeness / effective axiomatization	holds	fails (validity is not definable)
Set of validities	recursively enumerable	not even arithmetical
Categorical for $N$ , $R$	impossible	yes
Defines infinite, cardinalities	impossible	yes

Second-order axioms versus first-order schemas

The contrast is sharpest at the induction principle, which appears in both logics but means different things. The second-order induction postulate is the single sentence

\forall X (X 0 \land \forall y (X y \to X S y) \to \forall y X y),

whereas its first-order counterpart is a schema — the infinite set of all sentences

φ (0) \land \forall y (φ (y) \to φ (S y)) \to \forall y φ (y)

as $φ$ ranges over first-order formulas with one free variable.

The difference is which subsets the principle reaches. A model of the second-order postulate satisfies induction for every subset of its universe containing $0^{A}$ and closed under $S^{A}$ — so that subset must be the whole universe, forcing the model to be $N$ . A model of the first-order schema satisfies induction only for the definable subsets; undefinable subsets can escape it. A nonstandard model of $Th (N; 0, S)$ with $Z$ -chains satisfies the first-order schema — the set of standard points is not definable, so no instance of the schema pins it down — yet violates the second-order postulate outright.

The two induction principles differ in reach. The first-order schema constrains only the definable subsets; the second-order sentence constrains every subset of the universe.

The single sentence characterizes $N$ because it speaks about subsets no effective calculus can enumerate, which is why no effective calculus is complete for it. Expressive power and metatheoretic tameness trade off directly: Skolem functions and many-sorted logic keep second-order variables as a bookkeeping device over a first-order core, while general structures recover every lost metatheorem by shrinking the range of the quantifiers.

Enderton, §4.1. The additional symbols, the two satisfaction clauses, Examples 1–5, and Theorems 41A–41C are drawn from this section; the standard semantics quantifies over the full power set, which is the source of both the expressive gains and the metatheoretic failures. ↩