Reference request: eliminating function symbols in predicate logic

Question

Here is a basic technique in logic which seems well-known in folklore, but which I haven’t managed to find written down anywhere. $\newcommand{\T}{\mathbf{T}}$

Fact. Let $\Sigma$ be a signature (in the sense of predicate logic; i.e. sets of “function symbols” and “predicate symbols”, equipped with natural-number arities). Then there is a purely relational signature $\bar{\Sigma}$ and a theory $\T_\Sigma$ over $\bar{\Sigma}$, together with a translation from $L_\Sigma$ to $L_{\bar{\Sigma}}$ which is conservative modulo $\T_\Sigma$, i.e. $\varphi \vdash \psi$ over $\Sigma$ if and only if $\bar{\varphi} \vdash_{\T_\Sigma} \bar{\psi}$ over $\bar{\Sigma}$.

The idea is to replace each $n$-ary function of $\Sigma$ by an $(n+1)$-ary predicate in $\bar{\Sigma}$, and axioms in $\T_\Sigma$ stating that this predicate is functional.

Does anyone know a good citable source for some version of this technique?

(This is closely related to taking extensions by definitions, which is well-treated in the literature. It is straightforward to deduce this from the standard conservativity results for extensions by definitions, but it’s not quite a one-liner.)

Answer 1

The techique is in Bell & Machover: A course in mathematical logic, ch 2 §10 as theorem 10.5.

It states…

Select an $n$-ary function symbol $\mathbf f$ of $\mathcal L$, and let $\mathcal L'$ be obtained from $\mathcal L$ by excluding $\mathbf f$ and introducing a new $(n+1)$-ary predicate symbol $P$. We prove:

Theorem. For any $\mathcal L$-formula $\mathbf \alpha$ we can find an $\mathcal L'$-formula which is co-satisfiable with $\mathbf \alpha$ and an $\mathcal L'$ formula which is co-valid with $\mathbf \alpha$.

Google books link.