Beth definability theorem


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.


  • Evert Willem Beth, On Padoa’s method in the theory of definition , Indagationes Mathemathicae 15 (1953) pp.30-39.

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:

  • Michael Makkai, Duality and Definability in First Order Logic , Memoirs AMS no. 503, Providence 1993.

Last revised on January 4, 2015 at 09:06:21. See the history of this page for a list of all contributions to it.