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.

Related Concepts

• definability
• first-order logic
• conceptual completeness
• Robinson consistency theorem
• Craig interpolation theorem
• descent theory

References

• 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.