---
title: Second-Order Languages
module: Second-Order Logic and Beyond
moduleNumber: 9
lessonNumber: 1
order: 901
summary: >
  Second-order logic quantifies over relations and functions, not just
  individuals. Second-order Peano arithmetic and the second-order theory of the
  reals become categorical, and finiteness is definable by a single sentence.
  Compactness, completeness, and the Löwenheim–Skolem theorems all fail for the
  standard semantics.
topics: [Second-Order Logic and Beyond]
sources:
  - book: Enderton
    ref: "Ch. 4 — Second-Order Logic; §4.1 Second-Order Languages"
draft: false
---

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.[^enderton-41]

The formula

$$
\exists x\,(Px \to \forall x\, Px)
$$

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\,(Px \to \forall x\, Px),
$$

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](/logic/first-order-languages/first-order-languages)
we adjoin two new families of logical symbols.

- **Predicate variables.** For each positive integer $n$, the $n$-place
  predicate variables $X^n_1, X^n_2, \ldots$, each ranging over $n$-ary
  relations on the universe.
- **Function variables.** For each positive integer $n$, the $n$-place function
  variables $F^n_1, F^n_2, \ldots$, each ranging over $n$-ary operations on the
  universe.

The ordinary variables $v_1, v_2, \ldots$ 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 $Pt_1\cdots 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.

> **Definition (Second-order wff).** The well-formed formulas are generated
> from the atomic formulas by the first-order building operations together
> with: if $\varphi$ is a wff, then so are $\forall X^n_i\, \varphi$ and
> $\forall F^n_i\, \varphi$. A variable — individual, predicate, or function —
> occurs **free** exactly as in the first-order case, and a **sentence** is a
> wff in which no variable of any kind occurs free.

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.

$$
% caption: 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.
\begin{tikzpicture}[font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\tikzset{tier/.style={draw, minimum width=50mm, minimum height=12mm, align=center}}
\node[tier] (ind) at (0,0) {individual variables\\(range over points)};
\node[tier, draw=acc, very thick] (rel) at (0,1.7) {predicate variables\\(range over relations)};
\node[tier, draw=acc, very thick] (fun) at (0,3.4) {function variables\\(range over operations)};
\node[anchor=west, text=acc] at (2.75,2.55) {new in second order};
\draw[acc] (2.6,1.7) -- (2.7,1.7) -- (2.7,3.4) -- (2.6,3.4);
\end{tikzpicture}
$$

## Satisfaction with the new quantifiers

A structure remains what it was for [first-order logic](/logic/first-order-languages/structures-truth-and-satisfaction):
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 $|\fA|$,
- $s(X^n_i)$ is an $n$-ary relation on $|\fA|$,
- $s(F^n_i)$ is an $n$-ary operation on $|\fA|$.

The value $s(t)$ of a term is defined by the obvious recursion: if $F$ is a
function variable, $s(Ft_1\cdots t_n)$ applies the operation $s(F)$ to
$s(t_1), \ldots, s(t_n)$. Satisfaction of an atomic formula built from a
predicate variable $X$ reads off the relation $s(X)$ assigns:

$$
\models_{\fA} Xt_1\cdots t_n\,[s]
\quad\Longleftrightarrow\quad
\langle s(t_1), \ldots, s(t_n)\rangle \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.

> **Definition (Standard second-order satisfaction).** For a structure
> $\fA$ and assignment $s$,
> $$
> \models_{\fA} \forall X^n_i\, \varphi\,[s]
> \iff
> \text{for every } n\text{-ary relation } R \text{ on } |\fA|,\;
> \models_{\fA} \varphi\,[s(X^n_i \mid R)],
> $$
> $$
> \models_{\fA} \forall F^n_i\, \varphi\,[s]
> \iff
> \text{for every function } f : |\fA|^n \to |\fA|,\;
> \models_{\fA} \varphi\,[s(F^n_i \mid f)].
> $$

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 $\fA$,
and logical implication $\Sigma \models \sigma$ is defined exactly as before.
[General structures](/logic/second-order-logic/general-structures) relax this;
here the range of a second-order quantifier is fixed to everything on the
universe.

$$
% caption: 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.
\begin{tikzpicture}[font=\small]
\definecolor{acc}{HTML}{4A6FA5}
% universe box
\draw[black] (0,0) rectangle (2.6,3);
\node[anchor=south] at (1.3,3.05) {universe A};
\foreach \p in {(0.6,2.3),(1.5,2.5),(2.0,1.6),(0.8,1.2),(1.7,0.7),(1.1,0.4)}
  \fill \p circle(2.2pt);
% powerset stack
\begin{scope}[xshift=52mm]
  \foreach \i in {0,1,2,3}{
    \draw[black, fill=acc!10] (0.28*\i, 0.28*\i) rectangle ++(2.2,1.3);
  }
  \node[anchor=south west] at (0.9,1.75) {every subset};
\end{scope}
\draw[->, acc, thick] (2.75,1.5) -- (4.15,1.5);
\node[anchor=south, text=acc] at (3.45,1.55) {ranges over};
\node[align=center, anchor=north] at (5.1,0.05) {a single binding\\covers the power set};
\end{tikzpicture}
$$

## 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\,\bigl(\exists y\, Xy \to \exists y\,(Xy \wedge \forall z\,(Xz \to y \le z))\bigr).
$$

> **Worked example (Well-ordering distinguishes $\mathbb{N}$ from $\mathbb{Z}$).**
> Read the sentence above as "every nonempty subset has a $\le$-least element,"
> then test it on the two orderings.
>
> In $(\mathbb{N}; \le)$ it is true: each nonempty $X \subseteq \mathbb{N}$ has a
> least natural number, so the consequent holds for every value of $X$. In
> $(\mathbb{Z}; \le)$ it is false. Instantiate the outer $\forall X$ at the whole
> universe $X = \mathbb{Z}$, which satisfies the antecedent $\exists y\, Xy$ yet
> has no $\le$-least element, so
> $$
> \not\models_{(\mathbb{Z};\le)} \exists y\,(Xy \wedge \forall z\,(Xz \to y \le z))\,[X \mid \mathbb{Z}].
> $$
> A single second-order sentence, read against the full power set, decides
> well-ordering.

**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\,\bigl(X0 \wedge \forall y\,(Xy \to XSy) \to \forall y\, Xy\bigr).
$$

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

$$
\forall X\,\bigl[\exists y\,\forall z\,(Xz \to z \le y) \wedge \exists z\, Xz
\to \exists y\,\forall y'\,(\forall z\,(Xz \to z \le y') \leftrightarrow y \le y')\bigr].
$$

**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:

$$
\lambda_\infty:\quad
\exists X\,\bigl[\forall u\,\forall v\,\forall w\,(Xuv \to Xvw \to Xuw)
\wedge \forall u\,\neg Xuu \wedge \forall u\,\exists v\, Xuv\bigr],
$$

$$
\exists F\,\bigl[\forall x\,\forall y\,(Fx = Fy \to x = y) \wedge \exists z\,\forall x\, Fx \neq z\bigr].
$$

> **Worked example (Infinitude in one sentence).** Evaluate $\lambda_\infty$ in
> a finite structure and in $(\mathbb{N}; <)$.
>
> The sentence claims a relation $X$ that is transitive, irreflexive, and
> **serial** — every point has an $X$-successor, $\forall u\,\exists v\, Xuv$.
> In $(\mathbb{N}; <)$ the ordering $<$ witnesses it: $<$ is transitive and
> irreflexive, and each $n$ has $n < n+1$, so
> $$
> \models_{(\mathbb{N};<)} \lambda_\infty.
> $$
> In a finite set $A = \{a_1, \ldots, 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 $Xab$. Seriality
> fails at $a$, so the third conjunct is false under every choice of $X$, giving
> $$
> \not\models_A \lambda_\infty.
> $$
> Hence $\lambda_\infty$ is true in exactly the infinite structures. One sentence
> captures the class that first-order logic reaches only through the infinite
> set $\{\lambda_2, \lambda_3, \ldots\}$.

In first-order logic "there are at least $n$
things" needs a separate sentence $\lambda_n$ for each $n$, and infinitude is
captured only by the infinite set $\{\lambda_2, \lambda_3, \ldots\}$ — 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
$\lambda_\infty$.

### Comprehension

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

$$
\exists X^n\,\forall v_1\cdots\forall v_n\,\bigl[X^n v_1\cdots v_n \leftrightarrow \varphi\bigr]
$$

is valid: it says there is a relation holding of exactly the tuples that satisfy
$\varphi$. 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](/logic/second-order-logic/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.

> **Definition (Categorical).** A set of sentences is categorical if all of its
> models are isomorphic.

First-order logic cannot be categorical for any structure with an infinite
model: by the [Löwenheim–Skolem theorems](/logic/models-and-theories/compactness-and-lowenheim-skolem)
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\, Sx \neq 0, \qquad
\forall x\,\forall y\,(Sx = Sy \to x = y),
$$

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

$$
% caption: 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.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% standard chain
\node[anchor=east] at (-0.3,1.2) {standard};
\foreach \i/\lab in {0/0,1/1,2/2,3/3}{
  \fill[acc] (\i*1.1,1.2) circle(2.2pt);
  \node[anchor=south] at (\i*1.1,1.32) {\lab};
}
\fill[acc] (4.43,1.2) circle(0.9pt) (4.55,1.2) circle(0.9pt) (4.67,1.2) circle(0.9pt);
\foreach \i in {0,1,2}{\draw[->, acc] (\i*1.1+0.12,1.2) -- (\i*1.1+0.98,1.2);}
\draw[->, acc] (3.42,1.2) -- (4.28,1.2);
% extra Z-chain
\node[anchor=east] at (-0.3,0) {extra chain};
\fill[black] (0.18,0) circle(0.9pt) (0.3,0) circle(0.9pt) (0.42,0) circle(0.9pt);
\foreach \i in {1,2,3}{\fill[black] (\i*1.1,0) circle(2.2pt);}
\fill[black] (4.43,0) circle(0.9pt) (4.55,0) circle(0.9pt) (4.67,0) circle(0.9pt);
\draw[->, black] (0.6,0) -- (0.98,0);
\foreach \i in {1,2}{\draw[->, black] (\i*1.1+0.12,0) -- (\i*1.1+0.98,0);}
\draw[->, black] (3.42,0) -- (4.28,0);
% verdict
\node[anchor=west, align=left, text=acc] at (5.6,0.6) {induction over subsets\\excludes the extra chain};
\draw[acc, thick] (5.3,0.35) -- (5.05,0.35) -- (5.05,0) -- (5.3,0);
\end{tikzpicture}
$$

> **Worked example (Categoricity of second-order successor arithmetic).** Every
> model of the two successor axioms together with second-order induction is
> isomorphic to $(\mathbb{N}; 0, S)$.
>
> Let $\fA$ satisfy $\forall x\, Sx \neq 0$, $\forall x\,\forall y\,(Sx = Sy \to
> x = y)$, and the induction postulate. Define $h : \mathbb{N} \to |\fA|$ by
> $h(0) = 0^{\fA}$ and $h(n+1) = S^{\fA}(h(n))$. Its image
> $$
> \mathcal{R} = \{\,(S^{\fA})^n 0^{\fA} : n \in \mathbb{N}\,\}
> $$
> is a subset of $|\fA|$ containing $0^{\fA}$ and closed under $S^{\fA}$. Because
> standard induction quantifies over **every** subset, the induction postulate
> forces $\mathcal{R} = |\fA|$, so $h$ is onto.
>
> $h$ is one-to-one. By $\forall x\, Sx \neq 0$, no $h(k+1) = S^{\fA}(h(k))$
> equals $h(0) = 0^{\fA}$; and $\forall x\forall y\,(Sx = Sy \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 $\fA \cong (\mathbb{N}; 0, S)$.
> A general model may omit this very subset $\mathcal{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](/logic/models-and-theories/theories-elementary-classes-and-categoricity),
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 $\lambda_\infty$ shows why.

> **Theorem (Failure of compactness).** There is an unsatisfiable set of
> second-order sentences every finite subset of which is satisfiable.

The witness is $\{\neg\lambda_\infty, \lambda_2, \lambda_3, \ldots\}$. Each
finite subset mentions only $\neg\lambda_\infty$ and finitely many $\lambda_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](/logic/models-and-theories/compactness-and-lowenheim-skolem)
depended on exactly the finiteness that $\lambda_\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.

> **Theorem (Definability of cardinality).** There is a sentence in the
> second-order language of equality that is true in a set exactly when its
> cardinality is $2^{\aleph_0}$.

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^{\aleph_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.

> **Theorem (Nondefinability of second-order validity).** The set of Gödel numbers of
> valid second-order sentences is not definable in $\fN$ by any
> second-order formula.

The argument reruns [Tarski's undefinability theorem](/logic/incompleteness/incompleteness-and-undecidability):
the second-order theory $T^2$ of $\mathbb{N}$ is not second-order definable in
$\mathbb{N}$. Because the categorical sentence $\alpha$ — the arithmetic axioms
[$A_E$](/logic/arithmetic-and-definability/a-subtheory-and-representability)
conjoined with second-order induction — has only $\mathbb{N}$ as a model,

$$
\sigma \in T^2 \quad\Longleftrightarrow\quad (\alpha \to \sigma)\text{ 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 $\mathbb{N}$, $\mathbb{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\,\bigl(X0 \wedge \forall y\,(Xy \to XSy) \to \forall y\, Xy\bigr),
$$

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

$$
\varphi(0) \wedge \forall y\,(\varphi(y) \to \varphi(Sy)) \to \forall y\,\varphi(y)
$$

as $\varphi$ 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^{\fA}$ and closed under $S^{\fA}$ — so that
subset must be the whole universe, forcing the model to be $\mathbb{N}$. A model
of the first-order schema satisfies induction only for the **definable** subsets;
undefinable subsets can escape it. A [nonstandard model](/logic/models-and-theories/compactness-and-lowenheim-skolem)
of $\mathrm{Th}(\mathbb{N}; 0, S)$ with $\mathbb{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.

$$
% caption: 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.
\begin{tikzpicture}[font=\small]
\definecolor{acc}{HTML}{4A6FA5}
% left: definable subsets
\draw[black] (0,0) circle (1.5);
\node[anchor=south] at (0,1.55) {all subsets};
\draw[acc, fill=acc!10] (0,-0.15) ellipse (0.85 and 0.7);
\node[text=acc, font=\footnotesize] at (0,-0.15) {expressible};
\node[align=center, anchor=north] at (0,-1.7) {schema reaches\\the shaded part};
% right: all subsets
\begin{scope}[xshift=52mm]
  \draw[acc, thick, fill=acc!10] (0,0) circle (1.5);
  \node[anchor=south] at (0,1.55) {all subsets};
  \node[align=center, anchor=north] at (0,-1.7) {sentence reaches\\the whole disk};
\end{scope}
\end{tikzpicture}
$$

The single
sentence characterizes $\mathbb{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](/logic/second-order-logic/skolem-functions-and-many-sorted-logic)
keep second-order variables as a bookkeeping device over a first-order core,
while [general structures](/logic/second-order-logic/general-structures) recover
every lost metatheorem by shrinking the range of the quantifiers.

[^enderton-41]: 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.