nLab
Beth definability theorem

Idea

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.

References

For an English translation of Padoa’s contribution and historical background information consult:

A categorical generalization that uses methods of descent theory appears in: