The Beth definability theorem is a classical result in the model theory of first-order logic.
It is probably the oldest ‘result’ in model theory, as it goes back to Alessandro Padoa in 1900. The first proof for the case of predicate logic appeared in Beth (1953) whereas Alfred Tarski had treated the type-logical case in 1935. Modern proofs rely on the Robinson consistency theorem or the Craig interpolation theorem.
For an English translation of Padoa’s contribution and historical background information consult:
J. van Heijenoort (ed.), From Frege to Gödel - A Source Book in Mathematical Logic 1879-1931 , Harvard UP 1976.
M. Aiguier, F. Barbier, An institution-independent Proof of the Beth Definability Theorem , Studia Logica 85 no. 3 (2007) pp.333-359. (pdf)
A categorical generalization that uses methods of descent theory appears in: