Mathematical logic and foundations First-order logic Theorem

Herbrand's theorem

Builds on Skolem normal form Term Satisfiability Signature

Statement

Consider first-order logic without equality over a signature $\sigma$ with at least one constant symbol. Let $\varphi = \forall x_1 \cdots \forall x_n \, \psi(x_1, \dots, x_n)$ be a sentence in Skolem normal form, with $\psi$ quantifier-free. Then $\varphi$ is unsatisfiable if and only if there are finitely many tuples $\bar t_1, \dots, \bar t_k$ of closed terms with the following property. The conjunction $\psi(\bar t_1) \land \cdots \land \psi(\bar t_k)$ is unsatisfiable as a propositional formula, with its atomic sentences read as propositional variables.

Remarks

The instances $\psi(\bar t)$ with closed terms $\bar t$ are the ground instances of $\varphi$ . For the proof, suppose every finite set of ground instances is propositionally satisfiable. By propositional compactness, all ground instances are satisfiable at once by some assignment. This assignment defines a Herbrand structure, whose elements are the closed terms, and this structure is a model of $\varphi$ . The other direction holds because $\varphi$ implies each of its ground instances. Example: let $\varphi = \forall x \, (P(x) \land \neg P(f(x)))$ with a constant $c$ . The instances for $x = c$ and $x = f(c)$ contain $\neg P(f(c))$ and $P(f(c))$ , so their conjunction is unsatisfiable, and so is $\varphi$ . If $\sigma$ has no constant symbol, one adds one; without closed terms there are no ground instances.

Going deeper

For a student

Combined with Skolemization, the theorem gives a semi-decision procedure for validity in first-order logic. To test whether $\chi$ is valid, put $\neg \chi$ in Skolem normal form and search through larger and larger sets of ground instances. If $\chi$ is valid, the search ends; by Church's theorem it cannot always end when $\chi$ is not valid. The theorem is closely related to the compactness theorem and to Gödel's completeness theorem. With equality, the same holds after adding the equality axioms for $\sigma$ to $\varphi$ .

Reading path

To understand this page from the ground up, read these 5 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Satisfiability concept
Signature concept
Skolem normal form concept
Term concept
Herbrand's theorem statement

Tag	`VZ21F10WRS`
URI	`m2://VZ21F10WRS`
Kind	statement, theorem
Writing	W0 stub
MSC	03B10, 03F05, 03B35
Status	This copy of the site has no build data. Run `m2 status VZ21F10WRS`.
About	Satisfiability
Uses	Skolem normal form, Term, Satisfiability, Signature
Same as	Wikidata Q1930577 Wikipedia Herbrand's theorem
Changed	2 November 2026