# Can a sentence in a model-theoretic conservative extension be translated in the language of its reduct?

Let $L1$ and $L2$ two languages with $L1 \subset L2$ and $T1$ and $T2$ respectively a theory in $L1$ and $L2$. We say that $T2$ is a model-theoretic conservative extension of $T2$ iff every model $M1$ of $T1$ can be expanded to a model $M2$ of $T2$ (see Conservative extension ).
When we have $T1$ which proves something like $\forall x \exists !y F[x,y]$ where $F[x,y]$ is a formula with free variables x and y, we can define $L2=L1 \cup \{f\}$ where $f$ is a symbol constant with arity 2, and $T2=T1 \cup \{\forall xF(x,f(x))\}$ (see Conservativity theorem ), which is a model-theoretic extension of T1
Hence my question is the following. Is there any way to translate a sentence in $L2$ to a sentence in $L1$ ? For example, if $F$ is a $L2$-sentence, is there a $L1$-sentence $F'$ such as $T2 \vdash F \Leftrightarrow F'$ ? For example, if we take the theory of groups expressed in $L1$ which contains the symbols for the unity (constant), equality (2-ary relation), product (2-ary function), one can easily see that there is a natural model-theoretic conservative extension $L2$ equals $L1$ plus a symbol for the inverse (1-ary function). It would be convenient to use $L2$, and to say, not only for $L1$-sentences, that $T2 \vdash F$, hence $T1 \vdash$ (place here a formula not so much different from F). Because we use a stronger language and theory, but not so much.
My main concern is that in day-to-day mathematics, we use constants (0, empty set, etc.) and function symbols (for the pair, for sinus, etc.) introduced in that fashion and we say that everything is translatable in ZFC. Well, how ?

To see the "no" part, consider $L_1=T_1=T_2=\emptyset$, $L_2=\{f\}$ (a single function symbol); you can't write that $f$ is injective without referring to it, obviously.
On the other hand, if you have $L_2=L_1\cup\{f\}$, where $f$ is a ($\emptyset$-)definable function symbol, then if you take $\varphi(x,y)$ the definition of $f$, then you can just replace every occurence of $f$ in a sentence by its definition. For example $$(\forall x,y) (x\neq y)\rightarrow f(x)\neq f(y)$$ can be rewritten as $$(\forall x,y,z) (x\neq y)\rightarrow (f(x)=z\rightarrow f(y)\neq z)$$ and then as $$(\forall x,y,z) (x\neq y)\rightarrow (\varphi(x,z)\rightarrow \neg\varphi(y,z))$$