Transitivity of definable extensions of first-order languages

Question

Suppose we have first-order languages $L$, $L'$, and $L''$, such that $L'$ is a definable extension of $L$, and $L''$ is a definable extension of $L'$. Is $L''$ a definable extension of $L$? I think this is obvious, but it still needs proof.

Answer 1

If $L'$ is a definable extension of $L$, then there is some function $\phi$ which takes a first-order formula made in $L'$ and transforms it into a first-order formula made in $L$ such that $L'$ proves $\kappa$ iff $L$ proves $\phi(\kappa)$, and such that $\phi$ respects quantifiers, logical operators, and any atomic proposition which is in the language of $L$.

Consider in particular an extension by a single $j$-ary relation symbol $R$ with the definition $R(\vec{x}) :\equiv w(\vec{x})$, where $w$ is a formula with free variables in $\vec{x}$.

Then we see that we could define $R(\vec{x}) :\equiv \phi(w(\vec{x}))$. So we have defined $R$ in terms of the language of $L$.

And now consider an extension by a single $j$-ary function symbol $f$ with the definition $f(\vec{x}) = y :\equiv w(\vec{x}, y)$. Then we can equally define $f(\vec{x}) = y :\equiv \phi(w(\vec{x}, y))$. And node that since $L'$ implies $\forall \vec{x} \exists! y w(\vec{x}, y)$, it must be the case that $L$ implies $\phi(\forall \vec{x} \exists! y w(\vec{x}, y))$, which must be logically equivalent to $\forall \vec{x} \exists! y \phi(w(\vec{x}, y))$. So we have defined $f$ in terms of the language of $L$.