It is, in the sense you are using the terms, structures and not interpretations. That is so also in the definition that you quote (I looked up the section 31-44 that you mentioned). And it is structure in the definition you quote. For recall that the definition says "in every $\mathcal{L}$-interpretation."
A definition of the type given here is quite common. Essentially, what it does is to define a formula (with free occurrences of variables) to be true if the universally quantified version of the formula is true.
For technical reasons, allowing free occurrences of variables is useful. We will be wanting to define truth of sentences $\varphi$ in $\mathbf{M}$ by induction on the complexity of $\varphi$. So for example we will want to say that the sentence $\exists x \psi(x)$ is true in the structure $\mathbf{M}$ if for every element $m$ of $M$,
$\psi(m)$ is true in $\mathbf{M}$. That raises the immediate problem that $\psi(m)$ is not a sentence, you cannot put an object into a sentence.
There are two standard workarounds. One is to invent a new constant symbol for every element of $M$, extend the language $\mathcal{L}$ by adding these symbols. The other is to introduce assignments in the style that Halbeisen uses. If we do that, it is easier to work with formulas than with only those formulas that happen to be sentences.
There is a subtle difference between constant symbols in a language and the elements of a structure.
Let's start with a language, the language of groups. So we have a binary function symbol $m(x,y)$ for multiplication and a constant $e$ for the identity element. Any structure in this language should assign an element to this constant (and an operation to the function symbol). For example, in the additive group $\mathbb{Z}$ the element $0$ is assigned to $e$, but in the multiplicative group $\mathbb{Q} - \{0\}$ the element $1$ is assigned.
Now jump to satisfaction of sentences. If $\mathcal{M}$ is an $\mathcal{L}$-structure and $\varphi(x_1, \ldots, x_n)$ is an $\mathcal{L}$-formula, then of course, it would not really make sense to write $\mathcal{M} \models \varphi(x_1, \ldots, x_n)$ (see also footnote). In our example of the language of groups we could take the formula $m(x_1, x_2) = e$, what would $\mathcal{M} \models m(x_1, x_2) = e$ mean? Of course, this makes sense once we plug in elements from $\mathcal{M}$ for the free variables $x_1$ and $x_2$.
For example, for the multiplicative group $\mathbb{Q}$, asking whether or not $\mathbb{Q} \models m(1/3, 3) = e$ makes perfect sense. But we have to replace the symbols in our language by their interpretations first to give a final answer to this question. Doing that we arrive at "$1/3 \cdot 3 = 1$", which is true, so indeed $\mathbb{Q} \models m(1/3, 3) = e$. Note that "$m(1/3, 3) = e$" is no longer a formula (or sentence) in our language, so it will generally not make sense in any other structure (e.g. it does not make sense in $\mathbb{Z}$). But when replacing free variables by elements, and replacing all symbols by their interpretations, we can turn a formula into a statement that can be true or false in our structure. This is what $\mathbb{Q} \models m(1/3, 3) = e$ means, or more generally $\mathcal{M} \models \varphi(a_1, \ldots, a_n)$.
What often happens in model theory, is that we wish to fix some elements of a structure as parameters and act as if they were in the language in the first place. Formally what happens is this. Let $\mathcal{M}$ be an $\mathcal{L}$-structure.
- Extend our language to $\mathcal{L}_\mathcal{M}$ by adding a constant symbol $c_a$ for each $a \in \mathcal{M}$. Note that formally $c_a$ and $a$ are different objects: the first one is a constant symbol in the new language $\mathcal{L}_\mathcal{M}$ and the second one is an element in $\mathcal{M}$.
- The structure $\mathcal{M}$ was just an $\mathcal{L}$-structure, but we can naturally make it into an $\mathcal{L}_\mathcal{M}$-structure by interpreting every new constant symbol $c_a$ as $a$. This makes sense because by construction we had that $a$ is an element in $\mathcal{M}$.
Now comes the magic of this construction, which tells us why $c_a$ and $a$ are often used interchangeably. Even though they technically are different things! So read carefully where everything lives.
Let $\varphi(x_1, \ldots, x_n)$ be an $\mathcal{L}$-formula and let $a_1, \ldots, a_n \in \mathcal{M}$ be elements. As argued before, the question of whether or not $\mathcal{M} \models \varphi(a_1, \ldots, a_n)$ now makes sense. By the construction above, we also have constant symbols $c_{a_1}, \ldots, c_{a_n} \in \mathcal{L}_\mathcal{M}$, so we could also form the $\mathcal{L}_\mathcal{M}$-sentence $\varphi(c_{a_1}, \ldots, c_{a_n})$. Note that I say sentence now, because this has no free variables. Since we naturally view $\mathcal{M}$ as an $\mathcal{L}_\mathcal{M}$-structure, we can also ask whether or not $\mathcal{M} \models \varphi(c_{a_1}, \ldots, c_{a_n})$. To answer that question, we have to replace each constant symbol by their interpretation and we arrive at the same question we had before, namely $\mathcal{M} \models \varphi(a_1, \ldots, a_n)$.
What the above shows is that, viewing $\mathcal{M}$ as an $\mathcal{L}_\mathcal{M}$-structure, we have
$$
\mathcal{M} \models \varphi(c_{a_1}, \ldots, c_{a_n}) \quad \Longleftrightarrow \quad \mathcal{M} \models \varphi(a_1, \ldots, a_n).
$$
So the subtle difference between elements and constant symbols disappears in this way. Which is why many authors will not distinguish between them.
Footnote: some authors use $\mathcal{M} \models \varphi(x_1, \ldots, x_n)$ as an abbreviation for $\mathcal{M} \models \forall x_1 \ldots x_n \varphi(x_1, \ldots, x_n)$, which does make sense since then there are no longer free variables.
Best Answer
I think that there is no "compact" formalization of the required double substitution.
Assuming that [using $v_0, v_1, v_2$] :
we have :
with $v_2$ a new variable. This condition licences us to prove the equivalence.
Now we can perform the second substitution :
But, in general :
We can try with the approach to substitution in John Bell & Moshe Machover, A Course in Mathematical Logic (1977), page 57-on.
The "syntax" for substitution is : $\alpha(x,t)$ and the basic defintion is Definition 3.3 [page 59] :
Thus, considering again the formula :
we perform an alphabetic change using $v_n$, where $v_n$ is the first variable not occurring in $\varphi$, getting :
and then the substitution : $v_1 ← v_0$ (now $v_0$ is free for $v_1$ in the formula), to get :
The result will be :