Skolem Functions and Many-Sorted Logic

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 $φ \equiv ψ$ to mean that $φ$ and $ψ$ 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 φ (x, y) \equiv \exists F \forall x φ (x, F x) .

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 $φ (x, F x)$ hold for all $x$ , then for each $x$ the value $F x$ witnesses $\exists y$ . Read left to right it uses choice. Suppose a structure $A$ with assignment $s$ satisfies $\forall x \exists y φ$ . Then for each $a \in ∣ A ∣$ there is at least one $b$ with $⊨_{A} φ (x, y) [s (x ∣ a) (y ∣ b)]$ . Choosing one such $b$ for every $a$ defines a function $f$ with $f (a) = b$ , and then $⊨_{A} \forall x φ (x, F x) [s (F ∣ f)]$ .

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.

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} ψ (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} ψ (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.

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.

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 $F x$ . The next existential $\exists w$ is preceded by $\forall x$ and $\forall z$ , so $w$ becomes $G x z$ . 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, F x, z, G x z) .

For satisfiability the second-order prefix drops away: read $F, G$ as new function symbols $f, g$ , giving the universal sentence

θ : \forall x \forall z R (x, f x, z, g x z) .

In the expanded language $θ ⊨$ the original, and any model of the original expands to a model of $θ$ by interpreting $f, g$ as Skolem functions. So $θ$ 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.

Take $φ$ '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 $θ$ satisfies $θ ⊨ φ$ in the expanded language, and any model of $φ$ extends to a model of $θ$ by interpreting the new symbols as Skolem functions. So $φ$ and $θ$ are, in Enderton's phrase, equally satisfiable. Applying the same corollary to $\neg φ$ yields an existential formula that is valid if and only if $φ$ 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.

The proof is a reduction. Given any $σ$ , the equisatisfiability corollary applied to $\neg σ$ effectively produces an existential sentence valid exactly when $σ$ is valid. A decision procedure for existential validity would then decide arbitrary validity, contradicting Church's theorem. 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. 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, f u, g u, f f u, f g u, g f u, g g u, \dots,

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

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.

Let $Λ$ 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 $P t_{1} \dots t_{n}$ play the part of sentence symbols. Two cases split the outcome.

Case I — $Λ$ 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 $Λ$ , which does not exist.
Case II — $Λ$ 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^{H} (t_{1}, \dots, t_{n}) = f t_{1} \dots t_{n}$ ; and a predicate is interpreted by $v$ , with $⟨ t_{1}, \dots, t_{n} ⟩ \in P^{H}$ exactly when $v (P t_{1} \dots t_{n}) = T$ . The identity assignment then satisfies every universal sentence.

Worked example (Herbrand test of a non-implication). Does $\forall x \exists y P x y ⊨ \exists y \forall x P x y$ ? Decide it by a Herbrand expansion.

The implication holds iff ${\forall x \exists y P x y, \neg\exists y \forall x P x y}$ is unsatisfiable. Skolemize both members. The hypothesis becomes $\exists F \forall x P x F x$ , with equisatisfiable universal form $\forall x P x f x$ . The negated conclusion is $\forall y \exists x \neg P x y$ , Skolemized to $\forall y \neg P (g y) y$ . With $f, g$ new function symbols and one variable $u$ , the Herbrand universe is

u, f u, g u, f f u, f g u, g f u, \dots .

The instance set $Λ$ holds $P u f u, P (g u) (f g u), \dots$ and $\neg P (g u) u, \neg P (g f u) (f u), \dots$ . Read each atom as a sentence symbol and assign

v (P t_{1} t_{2}) = T \leftrightarrow t_{1} is shorter than t_{2} .

Every positive instance $P t (f t)$ is true, since $f t$ is longer than $t$ ; every negative instance $\neg P (g t) t$ is true, since $g t$ is not shorter than $t$ , so $P (g t) t = F$ . Thus $Λ$ is satisfiable in sentential logic, the Herbrand structure it builds models both universal sentences, and

\forall x \exists y P x y \neq ⊨ \exists y \forall x P x y .

The construction echoes the completeness proof: 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 gives a finite unsatisfiable subset of $Λ$ , from which first-order compactness follows. And enumerating $Λ$ while checking finite subsets by truth tables recovers the enumerability of validity: a valid $φ$ makes some finite stage unsatisfiable and detectable, while an invalid $φ$ 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 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_{1}^{i}, v_{2}^{i}, \dots$ 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 $⟨ i_{1}, \dots, i_{n} ⟩$ , 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 $⟨ i_{1}, \dots, i_{n}, i_{n + 1} ⟩$ , a set of $n$ -place function symbols taking arguments of sorts $i_{1}, \dots, 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 $P t_{1} \dots t_{n}$ is well formed only when the terms' sorts match the predicate's. A many-sorted structure $A$ supplies a nonempty universe $∣ A ∣_{i}$ for each sort and interprets the symbols respecting types: $P^{A} \subseteq ∣ A ∣_{i_{1}} \times \dots \times ∣ A ∣_{i_{n}}$ for a predicate, $f^{A} : ∣ A ∣_{i_{1}} \times \dots \times ∣ A ∣_{i_{n}} \to ∣ A ∣_{i_{n + 1}}$ for a function, and $c^{A} \in ∣ A ∣_{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.

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.

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 $φ \mapsto φ^{*}$ rewrites each sorted quantifier by relativizing it to its sort predicate:

\forall_{i} v_{n}^{i} ψ ⟼ \forall v (Q_{i} v \to ψ^{*}),

replacing $v_{n}^{i}$ by an ordinary variable $v$ , and every $=_{i}$ by plain $=$ . Semantically, a many-sorted $A$ becomes a one-sorted $A^{*}$ whose universe is the union $⋃_{i \in I} ∣ A ∣_{i}$ , with $Q_{i}$ interpreted as the slice $∣ A ∣_{i}$ .

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.

The translation is faithful, and one direction is immediate.

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 $Δ$ of one-sorted sentences rules that out — asserting each $Q_{i}$ is nonempty and that the function symbols respect sorts — and any model of $Δ$ converts back into a many-sorted structure. The two lemmas combine into the exact bridge.

Because $Δ$ 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)^{*}$ and $Δ$ 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 turn the badly behaved standard second-order semantics into the tame general semantics.¹

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). ↩

Naming witnesses

Equisatisfiability and undecidability

Herbrand expansions

Many-sorted logic

Reduction to one sort

Footnotes