---
title: General (Henkin) Structures
module: Second-Order Logic and Beyond
moduleNumber: 9
lessonNumber: 3
order: 903
summary: >
  General semantics reinterprets second-order logic by letting the predicate
  and function quantifiers range over a designated collection of relations and
  functions rather than all of them. Recast as many-sorted first-order logic
  with comprehension axioms, general second-order logic recovers a sound and
  complete calculus together with compactness and Löwenheim–Skolem, giving up
  the categoricity of the standard semantics. The ω-models of analysis show the
  trade.
topics: [Second-Order Logic and Beyond]
sources:
  - book: Enderton
    ref: "Ch. 4 — Second-Order Logic; §4.4 General Structures"
draft: false
---

The [standard semantics](/logic/second-order-logic/second-order-languages) for
second-order logic fixes the range of a predicate quantifier to be the full
power set: $\forall X^n$ means "for every $n$-ary relation whatsoever." That one
commitment produces both the categoricity of second-order arithmetic and the
failure of compactness, completeness, and Löwenheim–Skolem. General semantics
loosens exactly that commitment. It leaves the syntax of
[Section 4.1](/logic/second-order-logic/second-order-languages) untouched and
changes only what the second-order quantifiers range over — from all relations
to a **designated collection** of them. The reinterpretation makes second-order
logic a disguised form of [many-sorted first-order logic](/logic/second-order-logic/skolem-functions-and-many-sorted-logic),
and every metatheorem that first-order logic enjoys comes back with it.

## Second-order logic as a many-sorted language

The route to general structures runs through the many-sorted encoding. Build a
many-sorted language with $\aleph_0$ sorts: one individual sort, an $n$-place
predicate sort for each $n$, and an $n$-place function sort for each $n$. The
predicate and function **parameters** of the original second-order language
survive, taking individual-sort arguments; equality is used only between
individual terms.

Two new families of parameters connect the tiers.

- **Membership parameters.** For each $n$, a predicate parameter
  $\varepsilon_n$ taking one predicate-sort variable and $n$ individual terms.
  The atomic formula $\varepsilon_n X^n t_1 \cdots t_n$ says the tuple $\langle
  t_1, \ldots, t_n\rangle$ belongs to the relation denoted by $X^n$ — exactly
  the reading of the second-order atomic formula $X^n t_1 \cdots t_n$.
- **Evaluation parameters.** For each $n$, a function parameter $E_n$ taking one
  function-sort variable and $n$ individual terms, returning an individual term.
  The term $E_n F^n t_1 \cdots t_n$ denotes the value of the function $F^n$ at
  the given arguments — exactly the reading of $F^n t_1 \cdots t_n$.

Translating between the two languages is mechanical: attach the $\varepsilon_n$
and $E_n$ symbols to pass into the many-sorted language, strip them to return.
Their only purpose is to phrase second-order application as a first-order
predication, so the results of
[Section 4.3](/logic/second-order-logic/skolem-functions-and-many-sorted-logic)
apply verbatim.

$$
% caption: Second-order application recast as first-order predication. The
% membership parameter turns "the tuple satisfies the relation" into an atomic
% formula relating a predicate-sort argument to individual-sort arguments.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
\node[draw, minimum width=40mm, minimum height=12mm, align=center] (so) at (0,0) {second-order atom\\relation applied to a tuple};
\node[draw=acc, very thick, minimum width=44mm, minimum height=12mm, align=center] (ms) at (6.2,0) {many-sorted atom\\membership of tuple in relation};
\draw[->, acc, thick] (so.east) -- node[above, font=\footnotesize]{attach} (ms.west);
\draw[->, acc, thick] (ms.south) to[out=-150,in=-30] node[below, font=\footnotesize]{strip} (so.south);
\end{tikzpicture}
$$

Without loss of generality the membership and evaluation parameters can be taken
to mean genuine membership and genuine evaluation.

> **Theorem (Collapse to a general structure).** Let $\fA$ be a structure for the many-sorted
> language whose sort universes are pairwise disjoint. Then there is a
> homomorphism $h$ of $\fA$ onto a structure $\fB$ such that
> $h$ is the identity on the individual universe, the predicate universe of
> $\fB$ consists of actual relations on the individuals with
> $\varepsilon_n$ read as membership, and the function universe consists of
> actual functions with $E_n$ read as evaluation.

The homomorphism sends a predicate-sort object $Q$ to the relation
$\{\langle a_1, \ldots, a_n\rangle : \langle Q, a_1, \ldots, a_n\rangle \in
\varepsilon_n^{\fA}\}$ it induces through $\varepsilon_n$, and
similarly collapses each function-sort object to the operation it induces
through $E_n$. Because $h$ is the identity on individuals, where equality lives,
the [homomorphism theorem](/logic/first-order-languages/definability-and-elementary-equivalence)
gives $\models_{\fA} \varphi[s] \iff \models_{\fB}
\varphi[h \circ s]$. Once $\varepsilon_n$ and $E_n$ are pinned to membership and
evaluation they are determined by the rest of the structure, so they can be
discarded entirely.

## General structures

What remains after discarding $\varepsilon_n$ and $E_n$ is a structure carrying
its own designated relations and functions.

> **Definition (General pre-structure).** A general pre-structure
> $\fA$ for a second-order language is an ordinary structure together
> with, for each $n$, an **$n$-place relation universe** — a set of $n$-ary
> relations on $|\fA|$ — and an **$n$-place function universe** — a set
> of functions $|\fA|^n \to |\fA|$.

An assignment $s$ now sends each predicate variable to a member of the relation
universe and each function variable to a member of the function universe.
Satisfaction $\models^{G}_{\fA}$ is defined through the many-sorted
translation, and the two clauses that matter read off the designated universes
rather than the full power set:

$$
\models^{G}_{\fA} \forall X^n\, \varphi[s]
\iff
\text{for every } R \text{ in the } n\text{-place relation universe of } \fA,\;
\models^{G}_{\fA} \varphi[s(X^n \mid R)],
$$

$$
\models^{G}_{\fA} \forall F^n\, \varphi[s]
\iff
\text{for every } f \text{ in the } n\text{-place function universe of } \fA,\;
\models^{G}_{\fA} \varphi[s(F^n \mid f)].
$$

Against the [standard clauses](/logic/second-order-logic/second-order-languages),
the only change is "in the relation universe of $\fA$" in place of "on
$|\fA|$." A quantifier that once swept the entire power set now sweeps
whatever family the structure admits.

$$
% caption: Standard versus general semantics for a predicate quantifier. On the
% left the quantifier ranges over the whole power set; on the right, over a
% chosen subfamily the general structure carries with it.
\begin{tikzpicture}[font=\small]
\definecolor{acc}{HTML}{4A6FA5}
% standard: all subsets
\draw[acc, thick, fill=acc!10] (0,0) circle (1.5);
\node[anchor=south] at (0,1.55) {standard};
\node[align=center, font=\footnotesize] at (0,0) {all subsets\\of the universe};
% general: chosen subfamily
\begin{scope}[xshift=52mm]
  \draw[black] (0,0) circle (1.5);
  \node[anchor=south] at (0,1.55) {general};
  \draw[acc, thick, fill=acc!10] (-0.1,-0.1) ellipse (0.85 and 0.65);
  \node[align=center, font=\footnotesize, text=acc] at (-0.1,-0.1) {admitted\\subfamily};
  \node[font=\footnotesize] at (0.85,1.0) {excluded};
\end{scope}
\end{tikzpicture}
$$

A bare pre-structure is too permissive: with an impoverished relation universe,
formulas that ought to define relations would have nothing to name. The
restriction that fixes this is that the designated universes be
rich enough to contain everything the language can define.

> **Definition (General structure).** A general pre-structure is a **general
> structure** if every comprehension sentence is true in it — every
> generalization of a relation comprehension formula
> $\exists X^n \forall v_1 \cdots \forall v_n (X^n v_1 \cdots v_n \leftrightarrow
> \varphi)$, with $X^n$ not free in $\varphi$, and of the matching function
> comprehension formula.

Comprehension is the standing requirement that each formula-definable relation
actually appears in the relation universe. A standard structure satisfies every
comprehension sentence automatically, since its universe is the full power set;
a general structure must certify it. The comprehension sentences, written
$\Gamma$, are a fixed recursive set — this is what makes the whole reduction
effective.

$$
% caption: A general structure is a two-tier object: a universe of individuals
% below, and admitted universes of relations and functions above, closed under
% definability by the comprehension axioms.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% relations tier
\node[draw=acc, very thick, minimum width=32mm, minimum height=9mm, align=center] (rel) at (-2,1.6) {admitted relations};
\node[draw=acc, very thick, minimum width=32mm, minimum height=9mm, align=center] (fun) at (2,1.6) {admitted functions};
% individuals tier
\node[draw, minimum width=68mm, minimum height=11mm, align=center] (ind) at (0,0) {universe of individuals};
\draw[->, thick] (ind.north-|rel) -- (rel.south);
\draw[->, thick] (ind.north-|fun) -- (fun.south);
\node[anchor=west, align=left, font=\footnotesize, text=acc] at (3.9,0.8) {closed under\\comprehension};
\end{tikzpicture}
$$

> **Worked example (Comprehension forces definable sets into the universe).** In
> any $\omega$-model of analysis the set of even numbers belongs to the set
> universe.
>
> "Even" is defined by the first-order formula $\varphi(u):\ \exists v\,(u = v + v)$.
> The matching relation comprehension sentence
> $$
> \exists X^1\,\forall u\,\bigl(X^1 u \leftrightarrow \exists v\,(u = v + v)\bigr)
> $$
> is one of the sentences $\Gamma$ that every general structure must satisfy. In
> an $\omega$-model the individuals are $\mathbb{N}$ with $+$ standard, so the
> witnessing $X^1$ is exactly $\{0, 2, 4, \ldots\}$. The evens therefore lie in
> the set universe of every $\omega$-model, however sparse that universe is
> otherwise. Comprehension secures membership for each first-order-definable set
> the same way, which is what keeps the relation universe rich enough to
> interpret the language.

## The metatheorems return

Because a general structure is, by construction, a many-sorted first-order
structure satisfying the fixed axiom set $\Gamma$, every first-order metatheorem
transfers through the reduction of
[Section 4.3](/logic/second-order-logic/skolem-functions-and-many-sorted-logic).
A second-order sentence $\sigma$ is true in every general model of a set $\Sigma$
exactly when the many-sorted translation of $\sigma$ is a first-order
consequence of the translation of $\Sigma$ together with $\Gamma$. The
first-order theorems for that consequence relation then apply directly.

> **Theorem (Löwenheim–Skolem, general).** If a set of sentences in a countable
> second-order language has a general model, it has a countable general model —
> one in which every universe is countable.

> **Theorem (Compactness, general).** If every finite subset of a set of
> second-order sentences has a general model, the whole set has a general model.

> **Theorem (Enumerability, general).** For a recursively numbered language, the
> set of Gödel numbers of second-order sentences true in every general
> structure is recursively enumerable.

Each is proved by adjoining $\Gamma$ and invoking the corresponding many-sorted
theorem: for compactness, every finite subset of $\Sigma \cup \Gamma$ has a
model, so the whole set does; for enumerability, general validity is
many-sorted consequence of the recursive set $\Gamma$, hence recursively
enumerable. The enumerability theorem carries a corollary Enderton states
without developing.

> **Corollary.** There is a sound and complete deductive calculus for general
> second-order logic: $\Sigma \vdash \tau$ if and only if $\tau$ is true in
> every general model of $\Sigma$.

Completeness follows the same logic as the [first-order case](/logic/deductive-calculus/completeness-and-consistency):
the enumerability of general validity means the relation "true in every general
model" is recursively axiomatizable, and any recursively axiomatizable
consequence relation is captured by a deductive calculus. Knowing such a
calculus exists, there is little reason to develop one in detail. General
semantics restores the deductive completeness that the standard semantics lost.

## Absolute versus general second-order logic

The [standard semantics](/logic/second-order-logic/second-order-languages) is
**absolute** second-order logic; the designated-collection semantics is
**general** second-order logic.

> **Definition (Absolute vs. general).** In **absolute** second-order logic the
> meaning of the parameters is open to interpretation but the notion of "subset"
> is fixed — the quantifiers range over the true power set. In **general**
> second-order logic even the range of the second-order quantifiers is open to
> interpretation, so the logic reduces to first-order logic, much as axiomatic
> set theory speaks of sets and sets of sets while remaining a first-order
> theory.

Enlarging the class of admissible structures shrinks the implications that hold.
Every structure counts as a general model, so demanding truth in all of them is
a stronger demand than truth in the standard models alone: if $\sigma$ holds in
every general model of $\Sigma$, then it holds in every standard model too, and
$\Sigma \models \sigma$ in absolute second-order logic. The converse fails. With
$\Sigma = \varnothing$, the general validities are a recursively enumerable set,
whereas the absolute validities are [not even arithmetical](/logic/second-order-logic/second-order-languages),
so absolute validity strictly exceeds general validity.

$$
% caption: The expressiveness–tameness trade-off. Moving right buys categoricity
% and definability; moving left keeps a complete calculus, compactness, and
% Löwenheim–Skolem.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
\draw[->, thick] (-0.3,0) -- (10.3,0);
\foreach \x/\lab in {0.6/{elementary (order 1)}, 4.8/{general 2nd order}, 9.2/{absolute 2nd order}}{
  \fill (\x,0) circle(2.6pt);
  \node[align=center, anchor=south, font=\footnotesize] at (\x,0.12) {\lab};
}
\node[anchor=north, align=center, font=\footnotesize] at (1.2,-0.25) {complete, compact,\\Lowenheim-Skolem};
\node[anchor=north, align=center, font=\footnotesize] at (9.0,-0.25) {categorical,\\fixes sizes};
\node[anchor=north west, font=\footnotesize] at (3.6,-1.15) {more expressive};
\draw[->] (3.5,-1.0) -- (5.6,-1.0);
\end{tikzpicture}
$$

General second-order logic sits between the two extremes: more expressive than
first-order logic (it can still state comprehension and reason about relations
directly) yet tame enough to keep completeness, compactness, and
Löwenheim–Skolem. What it gives up in return is categoricity.
Second-order induction no longer characterizes $\mathbb{N}$, because a
general model can omit the very subset that second-order induction relies on.

> **Worked example (Second-order induction loses categoricity).** The single
> sentence
> $$
> \sigma_{\mathrm{ind}}:\quad \forall X\,\bigl(X0 \wedge \forall y\,(Xy \to XSy) \to \forall y\, Xy\bigr)
> $$
> is categorical under standard semantics yet has non-standard general models.
>
> Under the standard reading $\forall X$ ranges over the full power set, so
> $\sigma_{\mathrm{ind}}$ with the successor axioms forces every model to be
> $(\mathbb{N}; 0, S)$. Now read it generally. Adjoin a fresh constant $c$ and
> the sentences $c \neq S^n 0$, one for each numeral $S^n 0$. Every finite subset
> is generally satisfiable, since $c$ can name a large enough standard number, so
> general compactness yields a general model $\fA$ of $A^2_E$ with an element
> $c^{\fA}$ exceeding every numeral. This $\fA$ still satisfies
> $\sigma_{\mathrm{ind}}$: the set of standard points is not in $\fA$'s relation
> universe, so it is never a value of $X$ and cannot falsify the postulate.
> One sentence, categorical against the full power set, acquires non-standard
> models the moment the relation universe may omit a subset.

| | Elementary (first-order) | General second-order | Absolute second-order |
| --- | --- | --- | --- |
| Predicate quantifier ranges over | (no such quantifier) | admitted subfamily | full power set |
| Compactness | holds | holds | fails |
| Löwenheim–Skolem | holds | holds | fails |
| Complete calculus | holds | holds | fails |
| Categorical for $\mathbb{N}$ | no | no | yes |

## Models of analysis

The trade-off is concrete for second-order number theory, which logicians call
**analysis**: real numbers can be identified with sets of naturals, so
quantifying over sets of naturals is quantifying over reals. Take the
second-order language of arithmetic with parameters $0, S, <, +, \cdot, E$, and
let $A^2_E$ be the finitely axiomatized subtheory
[$A_E$](/logic/arithmetic-and-definability/a-subtheory-and-representability)
augmented with the second-order Peano induction postulate. Under the standard
semantics every model of $A^2_E$ is isomorphic to $\mathbb{N}$.

> **Definition (Model of analysis, $\omega$-model).** A **model of analysis** is
> a general model of $A^2_E$. It is an **$\omega$-model** if its individual
> universe is $\mathbb{N}$ with $0$ and $S$ standard — so $<, +, \cdot, E$ are
> standard as well — while its relation and function universes may be smaller
> than the full power set.

General models of $A^2_E$ can depart from $\mathbb{N}$ in two independent ways.
A [compactness](/logic/models-and-theories/compactness-and-lowenheim-skolem)
argument, adding constants exceeding every numeral, produces **nonstandard**
models with infinite numbers. Alternatively, a model can keep the standard
individual universe but admit a **non-absolute** set universe smaller than the
full power set of $\mathbb{N}$. Every countable general model is of the second
kind, since the full power set is uncountable; general Löwenheim–Skolem
guarantees countable models exist, and they cannot be absolute.

An $\omega$-model fixes the individuals and lets only the higher-tier universes
vary, and those are governed entirely by the set universe alone.

> **Theorem (Uniqueness of $\omega$-models of analysis).** Two $\omega$-models of analysis with the same one-place
> relation universe are equal.

A higher-arity relation $R$ can be compressed to a unary relation $\bar R$ by
coding tuples with the recursive, and hence
[arithmetically definable](/logic/computability-and-representability/recursive-functions),
sequence-encoding function. Comprehension then forces the set universe to
contain $\bar R$ exactly when the relation universe contains $R$, so the
one-place universe determines every other. An $\omega$-model can therefore be
identified with its set universe, a subclass of the power set $\mathcal{P}\mathbb{N}$,
though not every subclass qualifies, only those closed enough to satisfy the
comprehension sentences.

$$
% caption: The lattice of set universes. The full power set is the one absolute
% model; smaller admissible classes give the other omega-models, each a
% comprehension-closed subclass of the power set of the naturals.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% full power set at top
\node[draw=acc, very thick, fill=acc!10, minimum width=44mm, minimum height=9mm, align=center] (pw) at (0,3) {full power set: absolute model};
% set-theory model
\node[draw, minimum width=40mm, minimum height=8mm, align=center] (st) at (0,1.7) {sets in a transitive model};
% ramified
\node[draw, minimum width=40mm, minimum height=8mm, align=center] (ra) at (0,0.5) {smallest closed family};
\draw[->, acc, thick] (ra) -- (st);
\draw[->, acc, thick] (st) -- (pw);
\node[anchor=west, font=\footnotesize, text=acc] at (2.5,1.75) {larger admitted family};
\draw[->, acc] (2.4,0.8) -- (2.4,2.7);
\end{tikzpicture}
$$

Three $\omega$-models mark the range. The full power set $\mathcal{P}\mathbb{N}$
is the unique **absolute** model. The subsets of $\mathbb{N}$ lying in a
transitive model of set theory form an $\omega$-model. The **ramified
analytical sets** form the smallest natural $\omega$-model; they are built by
transfinitely iterating the operation "add every set definable over what we have
so far" until it closes off, which the general Löwenheim–Skolem theorem shows
happens at a countable ordinal. Each admits the same standard arithmetic on
individuals yet disagrees with the others on which second-order sentences hold,
a disagreement that is only possible because general semantics let the set
universe vary in the first place. That variation is the
trade: the metatheorems of first-order logic, in exchange for the categoricity
of the standard reading.[^enderton-44]

[^enderton-44]: Enderton, §4.4. The many-sorted recasting with the $\varepsilon_n$ and $E_n$ parameters, Theorem 44A, the definitions of general pre-structure and general structure via comprehension, the general Löwenheim–Skolem, compactness, and enumerability theorems, the absolute-versus-general comparison, and the treatment of $\omega$-models of analysis including Theorem 44B are all from this section.