Conservativity of language extension

Question

It is folklore that extending a language of classical first-order logic is conservative. That is, given two languages $L \subseteq L'$, a set of $L$-sentences $\Gamma$ and an $L$-sentence $\varphi$, then any derivation (proof tree) of $\varphi$ from $\Gamma$ in $L'$ can be transformed into a derivation of $\varphi$ from $\Gamma$ in $L$.

I'm looking for a detailed elementary proof is this fact. With "elementary" I mostly mean that it cannot use the completeness theorem (since the proof of the completeness theorem I know uses this fact). I'm mostly interested in the case where the derivations use natural deduction and classical logic.

Answer 1

The following works for essentially any common proof system (Hilbert calculus, sequent calculus, natural deduction, ...).

Take a proof of $\varphi$ from $\Gamma$ in $L'$. Substitute any fixed sentence (say, $\bot$) for all instances of predicates from $L'\smallsetminus L$ in the proof, and likewise, choose a variable $v$ that does not appear anywhere in the proof, and replace all topmost occurrences of subterms $F(t_1,\dots,t_n)$, $F\in L'\smallsetminus L$, with $v$. (This includes constants, for $n=0$.) You obtain a proof in $L$, and the transformation leaves $\Gamma$ and $\varphi$ unchanged.