I am trying to find (in a suitable language) a (simple) formula $\phi$, a term t, a structure $\mathcal{M}$ and an assignment b so that for $b':=b_{x/\overline{b}(t)}$ we get a different value for $\hat{b}(\phi[x/t])$ than for $\hat{b'}(\phi)$.
If any notation is unclear, please let me know.
Any ideas on how to approach the problem or any other suggestions?
IMO, we have to prove that $b(\phi[x/t])={b′}(\phi)$ for every $\phi$, i.e. that the operation of assigning denotation to variables commutes with substitution.
We start with $b : \text {Var} \to M$, where $M$ is the domain of $\mathcal M$; thus, $b(x)$ is an object in $M$.
And we have defined $\overline b$ such that $\overline b(u)=b(u)$ for every $u \in \text {Var}$.
Consider induction on the complexity of term $t$ :
(i) $t$ is a constant $c$.
Then $\overline b(t)=\overline b (c)=c^M$, because $\overline b(c)=c^M$ for all constant symbols.
This means that $b_{x/\overline b(t)}=b_{x/c^M}$, and thus $b'(x)=c^M$.
Consider now the formula $\phi$ with $x$ free.
We have that $b'(\phi)=b_{x/c^M}(\phi)$.
And $b(\phi[x/t])=b(\phi[x/c])=b_{x/c^M}(\phi)$, because the denotation of constant symbols is not affected by variable assignment functions.
(ii) $t$ is a variable $y \ne x$.
Then $\overline b(t)=\overline b (y)=b(y)$, because $\overline b(u)=b(u)$ for every variable $u$.
This means that $b_{x/\overline b(t)}=b_{x/b(y)}$, and thus $b'(x)=b(y)$.
Again, if formula $\phi$ has $x$ free, we have that $\phi[x/t]=\phi[x/y]$.
Thus, $b(\phi[x/t])=b(\phi[x/y])=b'(\phi)$.
(iii) $t$ is a "complex" term with function symbol $f$.
The proof is straightforward by induction hypothesis and the fact that the interpretation of a function symbol is not affected by variable assignments.