= Solution
For a <first-order signature> with at least one constant symbol, its <Herbrand universe> is the set of all <ground terms> built from its constant and function symbols. If necessary add a fresh constant to make this set nonempty. A <Herbrand structure> has exactly this domain; each constant denotes itself and each function symbol forms the corresponding syntactic <first-order term>. Its remaining choices are the <truth values> of the ground predicate atoms. For example, with constant $a$ and unary function $f$, the <Herbrand universe> is $\{a,f(a),f(f(a)),\ldots\}$.
One useful clausal form of <Herbrand's theorem> is the following. For a set $S$ of universally quantified, equality-free <first-order clauses>,
$$
\boxed{S\text{ is unsatisfiable}\quad\Longleftrightarrow\quad
\text{some finite set of ground instances of }S\text{ is propositionally unsatisfiable}.}
$$
Ground instances substitute <ground terms> for all variables. On the right, treat the ground predicate atoms as independent <Boolean variables>. Equivalently, $S$ is satisfiable if and only if it has a <Herbrand model>. A general <first-order sentence> can first be put into <Skolem normal form> and <clausal form>, with the new symbols included in the <Herbrand universe>.
An equivalent existential version says that a valid equality-free <first-order sentence> $\exists\bar x\,\theta(\bar x)$ with <quantifier-free formula> $\theta$ has finitely many ground tuples $\bar t_1,\ldots,\bar t_r$ such that $\bigvee_{i=1}^r\theta(\bar t_i)$ is propositionally valid, adding a constant if needed. This explains why a finite <ground resolution> refutation can establish a consequence involving infinitely many possible <ground terms>.
The equality-free qualification matters. If <first-order equality> is present, one must handle its axioms and use a term model modulo a suitable congruence, or use the corresponding theorem with equality. Literal syntactic term interpretation alone cannot model a consistent requirement such as $a=b$ for distinct constant symbols.
Back to article page
