Skip to main content
1 of 2

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.