I was reading the book "Foundations of Logic Programming" written by J.W.LIoyd. In the book, there were definitions of interpretation and model, and when it comes to Herbrand interpretation and model, I am having difficulties. It provided an example, but I did not understand it.

Example. Let $S$ be $\{ p(a), \exists x \neg p(x) \}$. Note that the second formula $S$ is not a clause. We claim that $S$ has a model. It suffices to let $D$ be the set $\{ 0,1\}$, assign 0 to $a$ and assign to $p$ the mapping which maps 0 to true and 1 to false. Clearly this gives a model for $S$. However, $S$ does not have an Herbrand model. This only Herbrand interpretations for $S$ are $\emptyset$ and $\{ p(a)\}$. But neither of these is a model for $S$.

In my understanding, by assigning 0 to $a$ and 1 to $x$ to the formulas of $S$ make them true:

$$ p(0) = true $$

$$ \exists x \neg p(x)[x/1] = \neg p(1) = true $$

Therefore, $\{ 0,1\}$ is a model for $S$ But I did not really understand how do we know $[a=0,x=1]$ is not a Herbrand model for $S$.

Could anyone explain to me? Thanks in advance.

  • $\begingroup$ I'm voting to close this question as off-topic because: better suited for cs.SE $\endgroup$ – Hermann Gruber Dec 20 '19 at 7:22
  • 1
    $\begingroup$ Hello, this should be explained in detail in any introductory book to logic (for example: Boolos et al.: Computability and Logic ), most likely in the section on syntax and semantics of predicate logic. In short, a Herbrand model is a specific model where every term is interpreted as itself. In other words, the domain is the set of all ground terms you can construct for the input language. In your case the language is {a, p(.) } and neither 0 nor 1 are in there. $\endgroup$ – lambda.xy.x Dec 20 '19 at 11:02
  • $\begingroup$ As a side node, please keep in mind that a model consists of a domain (your set S) and an interpretation for each constant, function and predicate symbol (you did not state that part in your question). Two models can share the same domain but differ in their interpretations. $\endgroup$ – lambda.xy.x Dec 20 '19 at 11:04
  • $\begingroup$ One more comment, if you need a free logic textbook, the open logic project has a quite extensive one. I haven't used it myself yet though. $\endgroup$ – lambda.xy.x Dec 20 '19 at 11:13