 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)),\dots \}$.

One useful clausal form of Herbrand's theorem is the following. For a set $S$ of universally quantified, equality-free first-order clauses,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,\dots ,{\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.