Herbrand universe ($\mathrm{HU}(\sigma )$)

The set of all ground terms over a first-order signature $\sigma$. Add a fresh constant if the first-order signature has none, so that this domain is nonempty. A constant $a$ and unary function $f$ give the Herbrand universe $\{a,f(a),f(f(a)),\dots \}$.

The set of all ground atoms formed using a Herbrand universe and the signature's predicates.

A first-order structure whose domain is the Herbrand universe, with constants denoting themselves and function symbols acting by syntactic term formation. Its predicates are specified by assigning truth values to ground atoms. With first-order equality, ordinary equality of syntactic terms imposes additional restrictions; more general term models may require quotienting by a congruence.

Equivalently, the predicate meanings of a Herbrand interpretation correspond to a subset of its Herbrand base.

A Herbrand structure satisfying the specified first-order sentences or first-order clauses.

For a satisfiable equality-free universal logical conjunction of Horn clauses, intersecting the sets of true ground atoms of its Herbrand models gives another Herbrand model, contained in every one of them. A ground atom is true in this least Herbrand model exactly when it holds in every Herbrand model. Positive existential sentences are true in the least Herbrand model exactly when they follow from the Horn clauses; allowing negated atoms makes this equivalence fail. For example, the least Herbrand model of $\forall x(P(x)\to Q(x))$ over a single constant $a$ makes both predicates empty and satisfies $\exists x\neg P(x)$, whereas the first-order structure making both predicates universal is a countermodel to that consequence.

A set of universally quantified equality-free first-order clauses is unsatisfiable if and only if some finite set of its ground instances is propositionally unsatisfiable. Equivalently, such a set is satisfiable if and only if it has a Herbrand model. General first-order sentences can first undergo Skolemization. A fresh constant is added if needed to make the Herbrand universe nonempty; first-order equality requires its corresponding equality treatment.