I am reading Van Dalen's Logic and Structure (5th ed.), and I am confused about the following part (Lemma 4.3.8).
$\mathfrak A$ is isomorphically embedded in $\mathfrak B$ $\iff$ $\mathfrak {\hat B}$ is a model of $Diag(\mathfrak A)$
My question is, why is it written $\mathfrak {\hat B}$ instead of $\mathfrak B$?
I understand that $\mathfrak {\hat B}$ is the model that has the elements of $|{\mathfrak B}|$ as additional constants, but I don't see why it needs to be $\mathfrak {\hat B}$. In the proof that follows, symbols without hats are also used, for example:
${\mathfrak A} \models P_i(\overline{a_1}, \dots, \overline{a_n}) \iff {\mathfrak B} \models P_i(\overline{f(a_1)}, \dots \overline{f(a_n)})$
Define a mapping $f: |\mathfrak A| \rightarrow |\mathfrak B|$ by $f(a)=(\overline{a})^{\mathfrak B}$.
but again, I don't know why.
$\mathfrak {\hat B}$ is needed here to be a model of $Diag(\mathfrak A)$ since $\mathfrak B$ is not a model of $Diag(\mathfrak A)$ and $Diag(\mathfrak A)$ is the set of true closed $L(\mathfrak A)$-atoms and true negations of closed $L(\mathfrak A)$-atoms in $\mathfrak A$.
If we assume $\mathfrak A$ is isomorphically embedded in $\mathfrak B$, then the $f$ in your following step ${\mathfrak A} \models P_i(\overline{a_1}, \dots, \overline{a_n}) \iff {\mathfrak B} \models P_i(\overline{f(a_1)}, \dots \overline{f(a_n)})$ is an isomorphism and $\mathfrak {\hat B}$ is defined as the model that has the elements of $|{\mathfrak B}|$ as additional constants, we can then simply interpret any $\overline{f(a_i)}$ in $\mathfrak B$ as $\overline{a_i}$ in $\mathfrak {\hat B}$ (note in $\mathfrak B$ we can only express an arbitrary term $f(a_i)$ without a name in general). And also recall all isomorphisms/homomorphisms between two structures in model theory are really defined via atomic formulas, so we can then see $\mathfrak {\hat B}$ is a model of $Diag(\mathfrak A)$, not $\mathfrak B$ in general.
And your another example of defining a mapping $f: |\mathfrak A| \rightarrow |\mathfrak B|$ by $f(a)=(\overline{a})^{\mathfrak B}$ is used to prove the other direction, and again similarly in order to prove such defined $f$ is an injection during the complete proof, $\mathfrak {\hat B}$ is needed in the assumption to ensure there's a non-identity atomic wff such as $\mathfrak {\hat B} \models (a_1 \neq a_2)$ from $Diag(\mathfrak A)$ when $\mathfrak A \models (a_1 \neq a_2)$, because by assumption we have $\mathfrak {\hat B}$ models $Diag(\mathfrak A)$. And then per the construction of $f$ above $f(a)$ always has a name $\overline{a}$ in $\mathfrak B$ now, we also have $\mathfrak B \models (a_1 \neq a_2)$, thus $f(a_1) \neq f(a_2)$.