= Least Herbrand model
{title2=$\mathcal H_F=\bigcap\{\mathcal H:\mathcal H\text{ is a Herbrand model of }F\}$}
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.
Back to article page
