We will use the following fact: $\exists x\phi$ , by definition, is $\neg\forall x\neg\phi$ , which is translated to $\neg\forall x(\pi_{\forall}(x)\rightarrow\neg\phi^{\pi})$ , and, by definition, the latter is just $\exists x(\pi_{\forall}(x)\wedge\phi^{\pi})$ .

First, we define a function $\pi$ from the set of parameters of $L_{0}$ into the set of formulas of $L_{1}$ . For every parameter except $f$ , let $\pi$ be the identity interpretation ($\pi$ itself is not an interpretation, as no theory in $L_{1}$ was defined so far, but we can still use the definition of the identity interpretation to define the function $\pi$ ). Now, we define $\pi_{f}=Pv_{1}\ldots v_{n}v_{n+1}$ .

Second, given $\pi$ , for every formula $\pi$ of $L_{0}$ , we can define $\phi^{\pi}$ as before (the definition of $\phi^{\pi}$ does not depend on the theory in $L_{1}$ ).

Finally, we define a set $\Sigma$ of formulas of $L_{1}$ as follows, $\Sigma=\{\sigma^{\pi}|\sigma\in T\}\cup\tau$ where $\tau=\forall v_{1}\ldots\forall v_{n}(\pi_{\forall}(v_{1})\rightarrow\ldots\rightarrow\pi_{\forall}(v_{n})$ $\rightarrow\exists x(\pi_{\forall}(x)\wedge\forall v_{n+1}(\pi_{f}\leftrightarrow v_{n+1}=x)))$ . In other words, $\Sigma$ contains all interpretations of the sentences of $T$ , plus a sentence $\tau$ that ensures that $P$ defines a function on the universe defined by $\pi_{\forall}$ with the range in the universe. A few words why we need to add this additional sentence. The way we define translations of wffs containing function symbols is such they do not ensure the existence of any value of the function, but only says something about the value if it exists. For example, even a sentence something like $\forall x\exists yfx=y$ is translated to $\forall x(\pi_{\forall}(x)\rightarrow\exists y(\pi_{\forall}(y)\wedge\forall z(\pi_{f}(x,z)\rightarrow z=y)))$ , which is literally translated as “for every $x$ in the universe there is $y$ in the universe such that for every $z$ if $z$ is a value of the function then $z=y$ ”, not ensuring the existence at all. So, we need to add $\tau$ explicitly. Now, it can be shown by the definition, that if $\sigma$ is a sentence of $L_{0}$ , then $\sigma^{\pi}$ is a sentence of $L_{1}$ . Hence, $\Sigma$ consists of sentences.

$\Sigma$ is not a theory. Indeed, if $\Sigma$ were a theory, then $\Sigma$ would be equal to $\mbox{Th}\mbox{Mod}\Sigma$ (see Exercise 3 of Section 2.6). At the same time, the latter contains all valid sentences, some of which, such as $\forall xx=x$ , are neither translations of any sentences of $L_{0}$ nor $\tau$ . So, we need to consider a larger set of formulas of $L_{1}$ , namely, $T'=\mbox{Cn}\Sigma$ . $T'$ is a theory. We show that $\pi$ is an interpretation of $L_{0}$ into $T'$ . For all parameters of $L_{0}$ except for $f$ , the definition of $\pi$ as the identity interpretation ensures that equations (i) and (ii) hold, see pages 167-168. For example, $\exists v_{1}\pi_{\forall}$ , which is $\exists v_{1}v_{1}=v_{1}$ , is valid, and, hence, is in $T'$ . Now, for $f$ , $\tau$ is exactly the sentence that ensures the correct definition of the interpretation.

$\sigma\in\pi^{-1}[T']$ iff $\sigma^{\pi}\in T'=\mbox{Cn}\Sigma$ iff $\Sigma\vDash\sigma^{\pi}$ . As we said, $\Sigma$ is not a theory, otherwise we would conclude “iff $\sigma^{\pi}\in\Sigma$ iff $\sigma\in T$ , as $\tau$ is not a translation”. However, we already know that if $\sigma\in T$ , then $\sigma^{\pi}\in\Sigma$ , $\Sigma\vDash\sigma^{\pi}$ , and $\sigma\in\pi^{-1}[T']$ , implying that $T\subseteq\pi^{-1}[T']$ , and $\pi$ is an interpretation of $T$ into $T'$ . To show that it is faithful, we need to show the opposite inclusion, i.e. $\pi^{-1}[T']\subseteq T$ , which holds iff $\Sigma\vDash\sigma^{\pi}$ implies $\sigma^{\pi}\in\Sigma$ (that is the “theory” property holds for translations), or, equivalently, $\sigma\in T$ .

If $T$ is inconsistent, then, obviously, $\pi^{-1}[T']\subseteq T$ holds. So, assume $T$ is consistent. Then, $\Sigma$ is consistent as well. Indeed, if $\mathfrak{A}$ is a model of $T$ , then we can consider a structure $\mathfrak{B}$ in $L_{1}$ which agrees with $\mathfrak{A}$ on all parameters except that instead of $f^{\mathfrak{A}}$ we have $P^{\mathfrak{B}}$ defined as $<d_{1},\ldots,d_{n},d_{n+1}>\in P^{\mathfrak{B}}$ iff $f^{\mathfrak{A}}(d_{1},\ldots,d_{n})=d_{n+1}$ . Then, all parameters of $^{\pi}\mathfrak{B}$ agree with those of $\mathfrak{A}$ , except for $P$ which needs additional verification. $f^{^{\pi}\mathfrak{B}}(d_{1},\ldots,d_{n})=d_{n+1}$ iff $\vDash_{\mathfrak{B}}\pi_{f}[[d_{1},\ldots,d_{n+1}]]$ iff $\vDash_{\mathfrak{B}}Pv_{1}\ldots v_{n+1}[[d_{1},\ldots,d_{n+1}]]$ iff $f^{\mathfrak{A}}(d_{1},\ldots,d_{n})=d_{n+1}$ , i.e. $f^{^{\pi}\mathfrak{B}}$ agrees with $f^{\mathfrak{A}}$ as well. In other words, $^{\pi}\mathfrak{B}=\mathfrak{A}$ , and for every $\sigma\in T$ , $\sigma$ is true in $^{\pi}\mathfrak{B}=\mathfrak{A}$ , implying that $\sigma^{\pi}$ is true in$\mathfrak{B}$ . Further, $\tau$ is true in $\mathfrak{B}$ as well (this follows from the fact that $P^{\mathfrak{B}}$ is defined via a function). Therefore, $\mathfrak{B}$ is a model of $\Sigma$ .

Now, suppose $\sigma\notin T$ . Then, $T\not\vDash\sigma$ , and $\tilde{T}=T;\neg\sigma$ is consistent. Then, $\tilde{\Sigma}=\Sigma;\neg\sigma^{\pi}$ is consistent, implying that $\Sigma\not\vDash\sigma^{\pi}$ , and, by the above argument, $\sigma\notin\pi^{-1}[T']$ . The contraposition of this is that, if $\sigma\in\pi^{-1}[T']$ then $\sigma\in T$ , exactly what we need.