Hils-Loeser Ex. 3.3.4: $T'$ is an expansion by definition of $T$ iff every $\scr L$-model of $T$ extends uniquely to a $\scr L'$-model of $T'$ The textbook is Hils-Loeser "A First Journey Through Logic".

Exercise 3.3.4. Let $T\subseteq T'$ be theories in languages $\scr L$ and $\scr L' \supseteq \scr L$,
respectively. Prove that $T'$ is equivalent to an expansion by definition of
$T$ if and only if every model of  admits a unique expansion to a model
of $T'$.

For the record, this is Hils-Loeser's definition of "expansion by definition":
$\newcommand{\vphi}{\varphi} \renewcommand{\%}{\textsf} \newcommand{\sL}{\mathscr{L}} \newcommand{\cforall}{\forall} \newcommand{\cexists}{\exists} \newcommand{\ssm}{\smallsetminus} \newcommand{\sm}{\setminus} \newcommand{\$}{\texttt} \newcommand{\barx}{\bar{\%x}}$

Let $T$ be $\sL$-theory, and suppose we have a larger language $\sL'\supseteq \sL$. Assume that

*

*for any $n$-ary relation symbol $\%R\in \sL'\sm\sL$, there is some associated $\sL$-formula $\vphi_\%R(\%x_1,\ldots, \%x_n)$ (no further specifications);

*for any $n$-ary function symbol $\%f\in \sL'\sm \sL$, there is some associated $\sL$-formula $\vphi_\%f(\%x_0,\ldots, \%x_n)$ s.t. $T \models \cforall\%x_1 \ldots \cforall\%x_n \cexists!\%x_0 \vphi_\%f$

*for any constant symbol $\%c\in \sL'\sm \sL$, there is some associated $\sL$-formula $\vphi_\%c(\%x_0)$ s.t. $T \models \cexists!\%x_0 \vphi_\%c$
Then, the $\sL'$-theory
$$\begin{aligned}
  E := T &\cup \{\cforall\%x_1 \ldots \cforall\%x_n \$(\vphi_\%R(\%x_1,\ldots, \%x_n) \leftrightarrow \%R\%x_1\ldots\%x_n \$) : \%R \in \sL'\ssm \sL \text{ relation symbol}\} \\
  &\cup \{\cforall\%x_1 \ldots \cforall\%x_n \; \vphi_\%f( \%f\%x_1\ldots\%x_n, \%x_1,\ldots, \%x_n) : \%f \in \sL'\ssm \sL \text{ function symbol}\} \\
  &\cup \{\vphi_\%c(\%c) : \%c \in \sL'\ssm \sL \text{ constant symbol}\}
\end{aligned}$$
is called an expansion by definition of $T$.


The forwards direction is easy (the bookkeeping/technical details are annoying though), but the backwards direction requires actually constructing for each relation/function/constant symbol $\%R,\%f,\%c \in \sL'\ssm \sL$ the associated $\sL$-formula $\vphi_{\%R,\%f,\%c}$. The only tool I know for this is the Beth definability theorem, which says that:

for $\sL$ be a language and $\$R\notin \sL$ be an $n$-ary relation symbol, and $T(\$R)$ be an $\sL\cup \{\$R\}$-theory; $T(\$R)$ explicitly defines the relation $\$R$

*

*i.e. there is $\sL$-formula $\vphi (\barx)$ s.t. $T(\$R) \models \cforall \barx\$(\$R(\barx) \leftrightarrow \vphi(\barx)\$)$
if and only if it implicitly defines $\$R$

*

*i.e. for any $\sL$-structure $\cal M$ with base set $M$, and any $n$-ary relations $R_1,R_2 \subseteq M^n$ s.t. $(\mathcal M, R_1)$ and $(\mathcal M, R_2)$ are both models of $T(\$R)$, we have $R_1 = R_2$.


So if $\sL'$ consisted of a single extra relation symbol $\%R$, then I could construct an $\sL$-formula $\vphi_\%R$ be be on my merry way. However, if there are more relation symbols, then Beth definability (applied to $T'_{-\%R}:= T'$ but remove any sentence in which $\%R$ occurs) can only cook up an $\sL'\ssm\{\%R\}$-formula $\vphi'_{-\%R}(\barx)$ s.t. $T' \models \forall \barx(\vphi'_{-\%R}(\barx) \leftrightarrow \%R\barx)$.
Then we know $\vphi'_{-\%R}(\barx)$ contains only finitely many extra relation symbols $\%R_1,\ldots, \%R_k \in \sL'\ssm \sL$, so we try to remove them/replace them with $\sL$-formulas. But it is unclear how to do this, since Beth definability can only cook up $\sL'\ssm\{\%R_i\}$-formula to replace each $\%R_i$, whereas we want sort of an $\sL \cup \{\%R_{i+1},\ldots, \%R_k\}$ formula to replace each $\%R_i$, so that we can replace the symbols one by one and ultimately get an $\sL$-formula $\vphi_\%R$ s.t. $T' \models \forall \barx(\vphi_{\%R}(\barx) \leftrightarrow \%R\barx)$ as desired.
Maybe rephrasing why the problem is a lot harder than the 1 relation symbol case: with 2 relation symbols $\%R_1,\%R_2$, it could be that all sentences in $T'$ involving $\%R_1$ also involve $\%R_2$, so although there could be many $\sL \cup \{\%R_1\}$-models of $T$ extending a given $\sL$-model $\mathcal M \models T$ (so we can't use Beth definability implicit def. $\implies$ explicit formula), there's only one $\sL \cup \{\%R_1,\%R_2\}$-model of $T$ extending $\cal M$. So $\%R_1,\%R_2$ "hold each other up", and we can't isolate them and deal with them one at a time.

This result seems like a super fundamental one, so I'm surprised I couldn't find anything online about it (sample query "expansion by definition iff unique extension model"). It also seems surprisingly hard. I also heard from a more learned logician that the Beth definability theorem is not very "robust", in the sense that it doesn't hold in more general logics, and he advised me to try to avoid using it. So I am also wondering if there is a simpler proof of this fundamental result.
 A: To prove this, you need a slightly strengthened form of the Beth Definability Theorem.

Let $L\subseteq L'$ be languages. Let $T'$ be an $L'$-theory, and let $\varphi$ be an $L'$-formula. The following are equivalent: (1) $\varphi$ is equivalent modulo $T'$ to an $L$-formula. (2) For all models $A,B\models T'$, if $A|L = B|L$, then $\varphi(A) = \varphi(B)$.

This is the form in which the theorem appears on Wikipedia and in Hodges's book Model Theory (Theorem 6.6.4 on p. 301).
You can prove this from the Craig Interpolation Theorem in just the same way that Hils and Loeser outline in Exercise 2.7.4. Here's a sketch.
The implication from (1) to (2) is clear. For the converse, let $L^*$ be the language obtained from $L'$ be replacing each symbol $S$ in $L'\setminus L$ by a distinct symbol $S^*$ of the same type, so that $L'\cap L^* = L$. Let $T^*$ and $\varphi^*$ be the $L^*$-theory and $L^*$-formula obtained from $T'$ and $\varphi$ by replacing all of the symbols in $L'$ by their doppelgangers in $L^*$. The hypothesis (2) implies that $T'\cup T^*\cup \{\varphi(c_1,\dots,c_n),\lnot \varphi^*(c_1,\dots,c_n)\}$ is inconsistent (where $c_1,\dots,c_n$ are $n$ new constant symbols). By compactness there is an $L'$-sentence $\theta'$, which is a consequence of $T'$, such that $\theta'\land \varphi(c_1,\dots,c_n) \models \theta^*\rightarrow \varphi^*(c_1,\dots,c_n)$. Let $\psi(c_1,\dots,c_n)$ be an interpolating $(L\cup \{c_1,\dots,c_n\}$-formula (by Craig Interpolation). Then the $L$-formula $\psi(x_1,\dots,x_n)$ is equivalent to $\varphi$ modulo $T'$, since $\varphi$ entails (modulo $T'$) $\theta'\land \varphi$, which entails $\psi$, and $\psi$ entails $\theta'\rightarrow \varphi$, which entails (modulo $T'$) $\varphi$.
Now in the situation of the exercise, we can applying the strengthened Beth Definability theorem to the formulas $R(x_1,\dots,x_n)$ for each $n$-ary relation symbol in $L'$, $f(x_1,\dots,x_n) = y$ for each $n$-ary function symbol in $L'$, and $y = c$ for each constant symbol in $L'$. Since $T\subseteq T'$, we find that there is an expansion $T''$ of $T$ by definitions such that $T'$ entails $T''$.
To see that $T'$ and $T''$ are equivalent, suppose $M$ is a model of $T''$. Then $M|L$ is a model of $T$, so $M|L$ has a unique expansion $M'$ to a model of $T'$. It follows that $M'\models T''$, and since $T''$ is an expansion of $T$ by definitions, $M' = M$, so $M\models T'$.
