Herbrand model

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.