 Solution

For each term $t$ define an $L_2$-formula $E_t(z)$ expressing its value. Use fresh bound variables at every step:Freshness includes avoiding all relevant free variables of the formula being translated. Define the atomic translation byand extend through the logical operations: $\sigma (\neg \theta )=\neg \sigma (\theta )$, $\sigma (\theta \to \eta )=\sigma (\theta )\to \sigma (\eta )$, and $\sigma (\forall x\theta )=\forall x\sigma (\theta )$. Fresh witnesses prevent variable capture and ensure the translation preserves the original free-variable set.

For an $L_1$-structure $A$, let $A^r$ have the graph relation of $f^A$ and singleton relation $\{c^A\}$. Induction on terms proves that $E_t(z)$ holds precisely when $z$ is the value of $t$. Induction on formulas then provesConversely every $L_2$-structure satisfying $\varphi ,\psi$ is uniquely the relational version of an $L_1$-structure on that same domain. Hence, for arbitrary possibly infinite $\Gamma$, semantic entailment on the left is equivalent to semantic entailment from $\sigma (\Gamma )\cup \{\varphi ,\psi \}$ on the right, with assignments retained in the free-formula case. Applying soundness theorem for first-order logic and Gödel's completeness theorem givesThe prohibition on completeness in the preceding direct equality question is local to that proof; here it supplies the clean semantic-to-syntactic transfer after the actual translation and model correspondence have been established.