Beth’s definability theorem a theorem for firstorder logic. A theory defines a term t implicitly if and only if an explicit definition of the term, on the basis of the other primitive concepts, is entailed by the theory. A theory defines a term implicitly if any two models of the theory with the same domain and the same extension for the other primitive terms are identical, i.e., also have the same extension for the term. An explicit definition of a term is a sentence that states necessary and sufficient conditions for the term’s applicability. Beth’s theorem was implicit in a method to show independence of a term that was first used by the Italian logician Alessandro Padoa (1868–1937). Padoa suggested, in 1900, that independence of a primitive algebraic term from the other terms occurring in a set of axioms can be established by two true interpretations of the axioms that differ only in the interpretation of the term whose independence has to be proven. He claimed, without proof, that the existence of two such models is not only sufficient for, but also implied by, independence.
Tarski first gave a proof of Beth’s theorem in 1926 for the logic of the Principia Mathematica of Whitehead and Russell, but the result was only obtained for first-order logic in 1953 by the Dutch logician Evert Beth (1908–64). In modern expositions Beth’s theorem is a direct implication of Craig’s interpolation theorem. In a variation on Padoa’s method, Karel de Bouvère described in 1959 a one-model method to show indefinability: if the set of logical consequences of a theory formulated in terms of the remaining vocabulary cannot be extended to a model of the full theory, a term is not explicitly definable in terms of the remaining vocabulary. In the philosophy of science literature this is called a failure of Ramsey-eliminability of the term. See also MODEL THEORY. Z.G.S.