# Prove that structure M is not Herbrand structure

I've been trying to solve the following problem, but I get a bit confused with the solution I get.

Here's the problem: Let's M be a structure with an universe all the terms with no variables. We know that the value of the term f(x) in M given evaluation v is v(x). Prove that M is not Herbrand structure.

My attempt to prove it:

By definition structure H is Herbrand if for every functional symbol f and elements of the Universe (which contains only terms with no variables)

$$t_1, ... , t_n$$ we have that $$f^H(t_1, ...,t_n)=f(t_1,...,t_n)$$ On the other hand we know evaluation functions are functions mapping elements of the Universe to variables.

So $$[\![f(x)]\!]^Hv=$$(by definition of evaluation)$$=f^H([\![x]\!]^Hv)=f^H(v(x))$$

On the other hand we want

$$f^H(x)=f(x)$$ By the definition of Herbrand structure. So here I get confused by the fact that the evalution v may be such that v(x)=x. Any suggestions how to prove it?

Let $$S$$ be a set of formulas (more exactly : clauses).

Let $$H$$ the Herbrand universe of $$S$$ (the domain of all ground (i.e. closed) terms) and $$I$$ an interpretation of $$S$$ over $$H$$.

In order that $$I$$ is an Herbrand model of $$S$$ we need that :

1) $$I$$ maps all constants in $$S$$ to themselves;

2) If $$f$$ is an $$n$$-place function symbol and $$h_1, \ldots, h_n$$ are elements of $$H$$, then $$I$$ must assign to $$f$$ a function $$f^{H}$$ that maps $$(h_1, \ldots, h_n)$$ to $$f^H(h_1, \ldots, h_n)$$ (an element of $$H$$).

But the variable $$x$$ is not in the Herbrand universe $$H$$, because it is not a closed term.

Thus, $$v(x)$$ is an element of the domain $$D$$ of the structure $$\mathcal M$$, and again $$v(x)$$ is not an element of $$H$$.

• Thank you! Clear and simple explanation! Jan 28, 2019 at 11:03
• @Zarrie - you are welcome :-) Jan 28, 2019 at 11:41