[EDIT: The theorem I call "Beth definability" below is apparently not generally called that (wikipedia notwithstanding; see https://math.stackexchange.com/questions/288450/two-forms-of-beths-theorem). Everything I've written below is still valid, both for the theorem actually called Beth definability and for the result I talk about, but I just want to make clear at the outset that my terminology is very nonstandard.]
Lindstrom's theorem is the statement that first-order logic is maximal among the class of regular logics with the compactness and downward Lowenheim-Skolem properties (for a precise statement, see e.g. Ebbinghaus/Flum's book, or "Model-Theoretic Logics" ed. Barwise/Feferman). I'm currently reading "The theorems of Beth and Craig in abstract model theory. I." by Makowsky and Shelah. On page 216, they say - referring to Lindstrom's Theorem on the maximality of first-order logic, and similar maximality theorems - that "most of the proofs of such maximality theorems also give a proof of Craig's theorem."
I interpret that sentence as saying that the proof methods can be adapted to yield a proof of Craig's theorem in the appropriate logic, rather than saying that Craig can be gotten as a corollary of a maximality result. However, I've started to wonder whether the latter might also be true. For example, there is a very straightforward proof of Beth's Definability Theorem$^1$ (a corollary of Craig's theorem) from Lindstrom's theorem, as follows: one defines for $L$ a regular logic the "Beth closure" of $L$, $L^b$, in a natural way, such that $L^b$ is also a regular logic; one shows that $L^b$ has the Beth definability property; and one shows that if $L$ is compact then so is $L^b$, and if $L$ has the Lowenheim-Skolem property then so does $L^b$. Now we're done: letting $L$ be first-order logic, we have that $L^b$ is an extension of first-order logic which is regular and (since $L$ itself has compactness and Lowenheim-Skolem) has the compactness and downward Lowenheim-Skolem properties. Hence by Lindstrom's Theorem, $L^b=L$ (or rather $L^b\equiv L$ for $\equiv$ appropriately defined), so first-order logic already has the Beth definability property.
One key feature of this proof, though, is that there is a natural definition for $L^b$ - sentences in $L^b$ come from sentences in $L$ in a straightforward way, and there is a unique reasonable choice for what the satisfaction relation should be. This breaks down terribly if we look at Craig's theorem$^2$, which says that for appropriate $\sigma, \tau$ there is a sentence $\phi$ satisfying some property $P_{\sigma, \tau}$, but that property does not uniquely determine $\phi$.
My question is whether there is a good way around this. Specifically: is there a way to derive Craig interpolation from Lindstrom's theorem?
$^1$ Informally, $L$ has the Beth definability property ($BDP$) if every implicit definition can be converted to an explicit definition, or more precisely if every sentence whose validity depends on only part of the vocabulary of the strucutre, is expressible using only that part of the vocabulary. Formally, $L$ has $BDP$ if whenever $\phi$ is an $L$-sentence with vocabulary $\Sigma$ and $\Sigma_0\subset\Sigma$ is such that $\mathcal{M}\upharpoonright \Sigma_0=\mathcal{N}\upharpoonright\Sigma_0\implies[\mathcal{M}\models\phi\iff\mathcal{N}\models\phi]$, then there is some $L$-sentence $\psi$ with vocabulary $\Sigma_0$ such that $\mathcal{M}\models\phi\iff\psi$ for all $\Sigma$-structures $\mathcal{M}$. Beth's definability theorem is the statement that first-order logic has $BDP$.
$^2$ $L$ has the Craig interpolation property if $\Sigma_0\cap\Sigma_1=\Sigma$, $\sigma$ is an $L$-sentence with vocabulary $\Sigma_0$ and $\tau$ is an $L$-sentence with vocabulary $\Sigma_1$ such that $\mathcal{M}\models \sigma\implies \tau$ for all $(\Sigma_0\cup\Sigma_1)$-structures $\mathcal{M}$, there is some $L$-sentence $\phi$ with vocabulary $\Sigma$ such that $\mathcal{M} \models\sigma\implies\phi\implies\tau$ for all $(\Sigma_0\cup\Sigma_1)$-structures $\mathcal{M}$.
