---
title: Skolem Functions and Many-Sorted Logic
module: Second-Order Logic and Beyond
moduleNumber: 9
lessonNumber: 2
order: 902
summary: >
  Skolem functions replace existential quantifiers with named witnesses,
  putting any first-order formula into a prenex form with all existentials —
  now over functions — pulled to the front. The Skolemized formula is
  equisatisfiable with the original, which reduces satisfiability to universal
  sentences and, through Herbrand expansions, to sentential logic. Many-sorted
  logic then adds several universes at once and reduces cleanly to ordinary
  one-sorted logic.
topics: [Second-Order Logic and Beyond]
sources:
  - book: Enderton
    ref: "Ch. 4 — Second-Order Logic; §4.2 Skolem Functions; §4.3 Many-Sorted Logic"
draft: false
---

A Skolem function names the witness that an existential quantifier only
promises. Replacing $\exists y$ by a function of the preceding universally bound
variables reorganizes any first-order formula into a rigid prenex shape: all
existentials, now over functions, pulled ahead of a block of universals over a
quantifier-free matrix. Here the second-order quantifiers leave first-order
logic exactly as strong as it was and serve only as bookkeeping. Existential
quantifiers are the obstacle to that shape, and Skolem functions remove them.

Throughout, write $\varphi \equiv \psi$ to mean that $\varphi$ and $\psi$ are
**logically equivalent** — each logically implies the other, so they hold in
exactly the same structures under the same assignments.

## Naming witnesses

Consider

$$
\forall x\,\exists y\, \varphi(x, y) \;\equiv\; \exists F\,\forall x\, \varphi(x, Fx).
$$

The right-hand form uses a one-place function variable $F$. Read from right to
left the equivalence is trivial: if some function $F$ makes $\varphi(x, Fx)$
hold for all $x$, then for each $x$ the value $Fx$ witnesses $\exists y$. Read
left to right it uses choice. Suppose a structure $\fA$ with assignment
$s$ satisfies $\forall x\,\exists y\,\varphi$. Then for each $a \in
|\fA|$ there is at least one $b$ with $\models_{\fA}
\varphi(x,y)[s(x \mid a)(y \mid b)]$. Choosing one such $b$ for every $a$ defines
a function $f$ with $f(a) = b$, and then $\models_{\fA} \forall x\,
\varphi(x, Fx)[s(F \mid f)]$.

> **Definition (Skolem function).** A function $f$ on $|\fA|$ that
> selects, for each $a$, a witness $b = f(a)$ making $\varphi(x, y)$ true is a
> Skolem function for $\forall x\,\exists y\,\varphi$ in $\fA$. Its
> existence uses the [axiom of choice](/logic/foundations/logic-as-a-mathematical-model).

$$
% caption: A Skolem function selects one witness per input. Where the original
% formula only promises that some witness exists for each x, the function names
% the choice, turning an existential over points into one function.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% left column: inputs
\node[anchor=south] at (0,2.7) {inputs (x)};
\foreach \i/\y in {1/2.0, 2/1.1, 3/0.2}{\fill[acc] (0,\y) circle(2.4pt); \node[anchor=east] at (-0.15,\y) {$a_\i$};}
% right column: candidate witnesses
\node[anchor=south] at (3.4,2.7) {candidate witnesses (y)};
\foreach \y in {2.35,1.85,1.35,0.85,0.35,-0.15}{\fill[black] (3.4,\y) circle(2.0pt);}
% chosen ones
\fill[acc] (3.4,1.85) circle(2.4pt);
\fill[acc] (3.4,0.85) circle(2.4pt);
\fill[acc] (3.4,0.35) circle(2.4pt);
\draw[->, acc, thick] (0.15,2.0) -- (3.25,1.85);
\draw[->, acc, thick] (0.15,1.1) -- (3.25,0.85);
\draw[->, acc, thick] (0.15,0.2) -- (3.25,0.35);
\node[anchor=west, text=acc] at (1.05,1.55) {f};
\node[align=center, anchor=north] at (1.7,-0.7) {the arrows are the graph of the Skolem function};
\end{tikzpicture}
$$

The argument iterates. Given a prenex formula whose quantifier prefix mixes
universals and existentials, take the leftmost existential that is preceded by
some universals, and replace its variable by a function of exactly those
preceding universally quantified variables. Starting from

$$
\exists y_1\,\forall x_1\,\exists y_2\,\forall x_2\,\forall x_3\,\exists y_3\, \psi(y_1, y_2, y_3),
$$

$y_1$ stays as an individual existential (nothing precedes it); $y_2$ becomes
$F_2 x_1$; $y_3$ becomes $F_3 x_1 x_2 x_3$. The result is

$$
\exists y_1\,\exists F_2\,\exists F_3\,\forall x_1\,\forall x_2\,\forall x_3\, \psi(y_1, F_2 x_1, F_3 x_1 x_2 x_3),
$$

with every existential — now over individuals and functions — pulled to the
front of a block of universals over a quantifier-free matrix.

> **Theorem (Skolem normal form).** For any first-order formula there is a
> logically equivalent second-order formula consisting of, in order: a string
> (possibly empty) of existential individual and function quantifiers; a string
> (possibly empty) of universal individual quantifiers; and a quantifier-free
> matrix.

$$
% caption: The target shape. All existential quantifiers, over individuals and
% Skolem functions, form a front block; a block of universal individual
% quantifiers follows; the matrix is quantifier-free.
\begin{tikzpicture}[font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node[draw=acc, very thick, fill=acc!10, minimum width=42mm, minimum height=13mm, align=center] (ex) at (0,0) {exists: individuals\\and functions};
\node[draw, minimum width=34mm, minimum height=13mm, align=center] (un) at (4.4,0) {for all:\\individuals};
\node[draw, minimum width=30mm, minimum height=13mm, align=center] (mx) at (8.2,0) {matrix\\(no bindings)};
\draw[->, acc, thick] (ex.east) -- (un.west);
\draw[->, acc, thick] (un.east) -- (mx.west);
\end{tikzpicture}
$$

> **Worked example (Skolem normal form of a concrete sentence).** Put
> $\forall x\,\exists y\,\forall z\,\exists w\, R(x,y,z,w)$ into Skolem normal
> form, then read off its equisatisfiable universal companion.
>
> Scan the prefix left to right. The first existential $\exists y$ is preceded by
> $\forall x$, so $y$ becomes $Fx$. The next existential $\exists w$ is preceded
> by $\forall x$ and $\forall z$, so $w$ becomes $Gxz$. Pulling the function
> existentials to the front,
> $$
> \forall x\,\exists y\,\forall z\,\exists w\, R(x,y,z,w)
> \;\equiv\;
> \exists F\,\exists G\,\forall x\,\forall z\, R(x, Fx, z, Gxz).
> $$
> For satisfiability the second-order prefix drops away: read $F, G$ as new
> function symbols $f, g$, giving the universal sentence
> $$
> \theta:\quad \forall x\,\forall z\, R(x, fx, z, gxz).
> $$
> In the expanded language $\theta \models$ the original, and any model of the
> original expands to a model of $\theta$ by interpreting $f, g$ as Skolem
> functions. So $\theta$ and the original sentence are equisatisfiable, though
> not logically equivalent.

## Equisatisfiability and undecidability

Skolem form still carries second-order quantifiers, but for questions of
satisfiability they can be dropped. Replacing each existentially quantified
function variable by a fresh **function symbol** removes the second-order
prefix, at the cost of logical equivalence — but not at the cost of
satisfiability.

> **Corollary (Skolem equisatisfiability).** For any first-order $\varphi$ there
> is a universal formula $\theta$ in a language expanded with new function
> symbols such that $\varphi$ is satisfiable if and only if $\theta$ is
> satisfiable.

Take $\varphi$'s Skolem normal form and read each existential function variable
$F_i$ as a new function symbol $f_i$; a zero-place existential individual becomes
a new constant. The resulting universal $\theta$ satisfies $\theta \models
\varphi$ in the expanded language, and any model of $\varphi$ extends to a model
of $\theta$ by interpreting the new symbols as Skolem functions. So $\varphi$
and $\theta$ are, in Enderton's phrase, "equally satisfiable." Applying the same
corollary to $\neg\varphi$ yields an **existential** formula that is valid if and
only if $\varphi$ is valid.

These reductions carry the general
satisfiability and validity problems to syntactically restricted
fragments — universal sentences for satisfiability, existential sentences for
validity — and the undecidability of the general problem transfers to those
fragments.

> **Corollary (Undecidable fragments).** In a recursively numbered
> language with a two-place predicate symbol and infinitely many $k$-place
> function symbols for each $k$: the set of Gödel numbers of satisfiable
> universal sentences is not recursive, and the set of Gödel numbers of valid
> existential sentences is not recursive.

The proof is a reduction. Given any $\sigma$, the equisatisfiability corollary applied to
$\neg\sigma$ effectively produces an existential sentence valid exactly when
$\sigma$ is valid. A decision procedure for existential validity would then
decide arbitrary validity, contradicting
[Church's theorem](/logic/incompleteness/incompleteness-and-undecidability).
Function variables can be replaced by predicate variables here, using a more
elaborate prefix; the analogue reduces satisfiability to $\forall_2$
formulas with predicate symbols.

## Herbrand expansions

The equisatisfiability corollary reduces satisfiability to universal sentences. Herbrand's method
takes one further step: the satisfiability of a set of universal sentences
reduces — in a weaker, sentential sense — to satisfiability in
[sentential logic](/logic/sentential-logic/truth-assignments-and-tautologies).
The construction makes a set of universal sentences generate its own model out
of pure syntax.

The carrier is the **Herbrand universe**: the set of all terms in the language.
With one variable $u$ and function symbols $f, g$, it contains

$$
u,\; fu,\; gu,\; ffu,\; fgu,\; gfu,\; ggu,\; \ldots,
$$

every term buildable from $u$ by the function symbols.

$$
% caption: The Herbrand universe as a term tree. Each node is a term; applying a
% function symbol descends one level. The universe is the set of all these
% syntactic objects, taken as points of a structure that names themselves.
\begin{tikzpicture}[font=\small, >=stealth, level distance=13mm,
  level 1/.style={sibling distance=30mm}, level 2/.style={sibling distance=15mm}]
\definecolor{acc}{HTML}{4A6FA5}
\node[draw=acc, very thick, circle, inner sep=1.5pt] {$u$}
  child {node[draw, circle, inner sep=1pt] {$fu$}
    child {node[font=\footnotesize] {$ffu$}}
    child {node[font=\footnotesize] {$gfu$}}}
  child {node[draw, circle, inner sep=1pt] {$gu$}
    child {node[font=\footnotesize] {$fgu$}}
    child {node[font=\footnotesize] {$ggu$}}};
\node[anchor=west, text=acc] at (2.6,-0.2) {apply f or g};
\end{tikzpicture}
$$

Let $\Lambda$ be the set of all **instances** of the universal sentences — drop
every universal quantifier and substitute Herbrand terms for the freed
variables. Each instance is quantifier-free, so it can be read as a formula of
sentential logic in which the atomic formulas $Pt_1\cdots t_n$ play the part of
sentence symbols. Two cases split the outcome.

- **Case I — $\Lambda$ is unsatisfiable in sentential logic.** Then the original
  set is unsatisfiable in first-order logic. A universal sentence implies all of
  its instances, so any first-order model of the set would yield a truth
  assignment satisfying $\Lambda$, which does not exist.
- **Case II — $\Lambda$ is satisfiable in sentential logic**, by some truth
  assignment $v$. Then $v$ builds a first-order model. Its universe is the
  Herbrand universe; function symbols are interpreted **autonymously**, each
  term naming itself, $f^{\fH}(t_1, \ldots, t_n) = ft_1\cdots t_n$; and
  a predicate is interpreted by $v$, with $\langle t_1, \ldots, t_n\rangle \in
  P^{\fH}$ exactly when $v(Pt_1\cdots t_n) = T$. The identity assignment
  then satisfies every universal sentence.

> **Theorem (Herbrand).** For a set $\Gamma; \varphi$ of sentences in a
> first-order language without equality, with $\Lambda$ the Herbrand expansion
> of the Skolemized set, either $\Lambda$ is unsatisfiable in sentential logic
> and $\Gamma \models \varphi$, or $\Lambda$ is satisfiable and the Herbrand
> structure $\fH$ is a model of $\Gamma$ in which $\varphi$ is false.

> **Worked example (Herbrand test of a non-implication).** Does
> $\forall x\,\exists y\, Pxy \models \exists y\,\forall x\, Pxy$? Decide it by a
> Herbrand expansion.
>
> The implication holds iff $\{\forall x\,\exists y\, Pxy,\; \neg\exists y\,\forall x\, Pxy\}$
> is unsatisfiable. Skolemize both members. The hypothesis becomes
> $\exists F\,\forall x\, PxFx$, with equisatisfiable universal form
> $\forall x\, Pxfx$. The negated conclusion is $\forall y\,\exists x\, \neg Pxy$,
> Skolemized to $\forall y\, \neg P(gy)y$. With $f, g$ new function symbols and
> one variable $u$, the Herbrand universe is
> $$
> u,\; fu,\; gu,\; ffu,\; fgu,\; gfu,\; \ldots.
> $$
> The instance set $\Lambda$ holds $Pu\,fu,\; P(gu)(fgu),\ldots$ and
> $\neg P(gu)u,\; \neg P(gfu)(fu),\ldots$. Read each atom as a sentence symbol and
> assign
> $$
> v(Pt_1 t_2) = T \iff t_1 \text{ is shorter than } t_2.
> $$
> Every positive instance $Pt\,(ft)$ is true, since $ft$ is longer than $t$;
> every negative instance $\neg P(gt)t$ is true, since $gt$ is not shorter than
> $t$, so $P(gt)t = F$. Thus $\Lambda$ is satisfiable in sentential logic, the
> Herbrand structure it builds models both universal sentences, and
> $$
> \forall x\,\exists y\, Pxy \;\not\models\; \exists y\,\forall x\, Pxy.
> $$

The construction echoes the [completeness proof](/logic/deductive-calculus/completeness-and-consistency):
a model is assembled from syntax, terms serving as their own denotations. It
also yields alternate proofs of first-order compactness and the enumerability of
validity that bypass the deductive calculus entirely. In Case I, sentential
[compactness](/logic/sentential-logic/compactness-and-effectiveness) gives a
finite unsatisfiable subset of $\Lambda$, from which first-order compactness
follows. And enumerating $\Lambda$ while checking finite subsets by truth tables
recovers the enumerability of validity: a valid $\varphi$ makes some finite stage
unsatisfiable and detectable, while an invalid $\varphi$ drives an endless model
construction.

## Many-sorted logic

Ordinary mathematics routinely runs several kinds of variable at once: Greek
letters for ordinals, capitals for sets, lowercase for elements, each ranging
over its own domain. Many-sorted logic makes that practice precise, and
[general structures](/logic/second-order-logic/general-structures) recast
second-order logic inside it.

Fix a nonempty set $I$ of **sorts**. The alphabet is typed throughout.

- **Variables.** For each sort $i$, variables $v^i_1, v^i_2, \ldots$ ranging over
  the universe of sort $i$.
- **Quantifiers.** A universal quantifier $\forall_i$ for each sort $i$.
- **Predicate symbols.** For each arity $n$ and each tuple of sorts $\langle i_1,
  \ldots, i_n\rangle$, a set of $n$-place predicate symbols of that sort.
- **Constant symbols.** For each sort $i$, a set of constant symbols of sort $i$.
- **Function symbols.** For each $\langle i_1, \ldots, i_n, i_{n+1}\rangle$, a set
  of $n$-place function symbols taking arguments of sorts $i_1, \ldots, i_n$ and
  returning a value of sort $i_{n+1}$.
- **Equality.** For some sorts $i$, an equality symbol $=_i$ comparing two terms
  of sort $i$.

Every term receives a unique sort by the typing rules, and an atomic formula
$Pt_1\cdots t_n$ is well formed only when the terms' sorts match the predicate's.
A **many-sorted structure** $\fA$ supplies a nonempty universe
$|\fA|_i$ for each sort and interprets the symbols respecting types:
$P^{\fA} \subseteq |\fA|_{i_1} \times \cdots \times
|\fA|_{i_n}$ for a predicate, $f^{\fA} : |\fA|_{i_1}
\times \cdots \times |\fA|_{i_n} \to |\fA|_{i_{n+1}}$ for a
function, and $c^{\fA} \in |\fA|_i$ for a constant. Truth and
satisfaction are defined as expected, with $\forall_i$ reading "for all members
of the universe of sort $i$." Because there is no cross-sort equality, whether
the universes overlap is immaterial — any many-sorted structure is elementarily
equivalent to one with pairwise disjoint universes.

$$
% caption: A two-sorted structure. Points and lines occupy separate universes;
% the incidence predicate relates a point-sort argument to a line-sort argument.
% Nothing forces the universes to overlap.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% points universe
\draw[black] (0,0) rectangle (2.6,1.6);
\node[anchor=south] at (1.3,1.65) {universe of sort: points};
\foreach \p in {(0.6,1.0),(1.3,0.6),(2.0,1.1)}{\fill[acc] \p circle(2.4pt);}
% lines universe
\begin{scope}[xshift=42mm]
  \draw[black] (0,0) rectangle (2.6,1.6);
  \node[anchor=south] at (1.3,1.65) {universe of sort: lines};
  \draw[acc, thick] (0.4,0.4) -- (2.2,1.2);
  \draw[acc, thick] (0.4,1.2) -- (2.2,0.5);
\end{scope}
\node[align=center, anchor=north] at (3.4,-0.3) {incidence relates a point of one sort to a line of the other};
\end{tikzpicture}
$$

### Reduction to one sort

Many-sorted logic is a convenience, not an extension: everything it can express
is already expressible with a single sort. Fix a one-sorted language with all
the predicate, constant, and function symbols of the many-sorted language, plus
one new one-place predicate symbol $Q_i$ for each sort $i$ — the predicate "is of
sort $i$." A syntactic translation $\varphi \mapsto \varphi^{\ast}$ rewrites each
sorted quantifier by **relativizing** it to its sort predicate:

$$
\forall_i v^i_n\; \psi \quad\longmapsto\quad \forall v\,(Q_i v \to \psi^{\ast}),
$$

replacing $v^i_n$ by an ordinary variable $v$, and every $=_i$ by plain $=$.
Semantically, a many-sorted $\fA$ becomes a one-sorted $\fA^{\ast}$
whose universe is the union $\bigcup_{i \in I} |\fA|_i$, with $Q_i$
interpreted as the slice $|\fA|_i$.

$$
% caption: The one-sorted encoding. The separate sort universes are poured into
% one universe, and each is recovered as the extension of its sort predicate,
% which relativizes the quantifiers.
\begin{tikzpicture}[font=\small, >=stealth]
\definecolor{acc}{HTML}{4A6FA5}
% two sorts
\draw[black] (0,0.9) rectangle (1.7,1.9);
\node[anchor=south, font=\footnotesize] at (0.85,1.9) {sort a};
\draw[black] (0,-0.5) rectangle (1.7,0.5);
\node[anchor=north, font=\footnotesize] at (0.85,-0.55) {sort b};
\draw[->, acc, thick] (2.0,0.7) -- (3.2,0.7);
% one universe with two labelled regions
\begin{scope}[xshift=34mm]
  \draw[black] (0,-0.6) rectangle (3.0,2.0);
  \node[anchor=south] at (1.5,2.0) {one universe};
  \draw[acc, fill=acc!10] (0.8,1.25) ellipse (0.7 and 0.5);
  \node[text=acc, font=\footnotesize] at (0.8,1.25) {Q for a};
  \draw[acc, fill=acc!10] (2.1,0.15) ellipse (0.7 and 0.5);
  \node[text=acc, font=\footnotesize] at (2.1,0.15) {Q for b};
\end{scope}
\end{tikzpicture}
$$

> **Worked example (Relativizing a two-sorted sentence).** Translate "every line
> has a point on it" into one-sorted logic and state its $\Delta$.
>
> Sorts $p$ (points) and $\ell$ (lines), with an incidence predicate $I$ of sort
> $\langle p, \ell\rangle$, make the sentence
> $$
> \sigma:\quad \forall_\ell y\,\exists_p x\, Ixy.
> $$
> Relativizing each sorted quantifier to its sort predicate $Q_p, Q_\ell$ and
> replacing sorted variables by ordinary ones,
> $$
> \sigma^{\ast}:\quad \forall v\,\bigl(Q_\ell v \to \exists w\,(Q_p w \wedge Iwv)\bigr).
> $$
> By the lemma below, $\sigma$ is true in a two-sorted $\fA$ exactly when
> $\sigma^{\ast}$ is true in its one-sorted encoding $\fA^{\ast}$. For the
> consequence direction the well-definedness set is needed: here $\Delta =
> \{\exists v\, Q_p v,\; \exists v\, Q_\ell v\}$, since there are no cross-sort
> function symbols to constrain. Then $\Gamma \models \sigma$ iff
> $\Gamma^{\ast} \cup \Delta \models \sigma^{\ast}$.

The translation is faithful, and one direction is immediate.

> **Lemma (Sort-erasing translation preserves truth).** A many-sorted sentence $\sigma$ is true in $\fA$ if
> and only if $\sigma^{\ast}$ is true in $\fA^{\ast}$.

The converse needs care, because a one-sorted structure need not come from a
many-sorted one: its sort predicates might be empty or not closed under the
functions. A finite set $\Delta$ of one-sorted sentences rules that out —
asserting each $Q_i$ is nonempty and that the function symbols respect sorts —
and any model of $\Delta$ converts back into a many-sorted structure. The two
lemmas combine into the exact bridge.

> **Theorem (Many-sorted consequence via one-sorted logic).** In the many-sorted language, $\Gamma \models \sigma$ if and
> only if $\Gamma^{\ast} \cup \Delta \models \sigma^{\ast}$ in the one-sorted
> language, where $\Gamma^{\ast} = \{\sigma^{\ast} : \sigma \in \Gamma\}$ and
> $\Delta$ is the set of sort-well-definedness sentences.

Because $\Delta$ is finite (indeed recursive) and the translation is effective,
the good behavior of one-sorted logic transfers wholesale. Compactness,
enumerability of validity, and Löwenheim–Skolem all hold for many-sorted logic,
each proved by pushing the problem through $(\cdot)^{\ast}$ and $\Delta$ to the
one-sorted theorem and pulling the model back.

| Theorem | One-sorted source | Many-sorted version |
| --- | --- | --- |
| Compactness | first-order compactness | every finitely satisfiable set of many-sorted sentences has a model |
| Enumerability | validity is r.e. | valid many-sorted sentences are r.e. |
| Löwenheim–Skolem | countable elementary submodel | a many-sorted structure has a countable elementarily equivalent one |

This pattern — encode a richer logic as many-sorted first-order logic,
relativize its quantifiers to sort predicates, inherit the metatheorems — is
exactly how [general structures](/logic/second-order-logic/general-structures)
turn the badly behaved standard second-order semantics into the tame general
semantics.[^enderton-4243]

[^enderton-4243]: Enderton, §4.2 (Skolem functions, the Skolem normal form theorem, Corollaries 42A–42B, Herbrand expansions and Herbrand's theorem) and §4.3 (many-sorted syntax and structures, the translation to one-sorted logic, Lemmas 43A–43B, Theorem 43C, and the inherited compactness, enumerability, and Löwenheim–Skolem theorems).