Prove that structure M is not Herbrand structure

Question

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?

Answer 1

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$.