Hi John, the least Herbrand model seems to be closely related to the Herbrand semantics you mentioned, but I understand it through the usual Tarski semantics.

The interpretation (called the [Herbrand structure](https://en.wikipedia.org/wiki/Herbrand_structure) on Wikipedia) is built out of syntactic material: it takes the universe to be the set of all ground terms and interprets constants and function terms as themselves. The construction is reminiscent of classifying categories in categorical logic. In the minimum Herbrand model, the true ground atoms are exactly those entailed by the axioms. This leads to a classic feature of Prolog called ["negation as failure"](https://en.wikipedia.org/wiki/Negation_as_failure): the negation of a ground atom is true in the minimum Herbrand model if the atom is not provable.

Because Prolog is a programming language first and a logical system second, it makes sense to fix the model. Otherwise, a Prolog program would have infinitely many interpretations! But you could drop this requirement and ask how Prolog works as a logical system, compared to say regular logic. I don't know Prolog well enough to know the answer, but this discussion has made me curious. When I have time I'll look into it.