= Solution
For each term $t$ define an $L_2$-formula $E_t(z)$ expressing its value. Use fresh <bound variables> at every step:
$$
E_x(z):=(z=x),\qquad E_c(z):=Q(z),\qquad E_{f(t)}(z):=\exists y\,[E_t(y)\land P(y,z)].
$$
Freshness includes avoiding all relevant <free variables> of the formula being translated. Define the atomic translation by
$$
\sigma(t_1=t_2):=\exists u\exists v\,[E_{t_1}(u)\land E_{t_2}(v)\land u=v],
$$
and 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 proves
$$
A,s\models\alpha\quad\Longleftrightarrow\quad A^r,s\models\sigma(\alpha).
$$
Conversely every $L_2$-structure satisfying $\phi,\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\{\phi,\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> gives
$$
\boxed{\Gamma\vdash\alpha\quad\Longleftrightarrow\quad\sigma(\Gamma)\cup\{\phi,\psi\}\vdash\sigma(\alpha).}
$$
The 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.
Back to article page
