mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...

, Beth definability is a result that connects implicit definability of a property to its explicit definability. Specifically Beth definability states that the two senses of definability are equivalent.

First-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

has the Beth definability property.

Statement

For first-order logic, the theorem states that, given a

theory A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be s ...

''T'' in the language ''L''' ⊇ ''L'' and a formula ''φ'' in ''L''', then the following are equivalent: * for any two models ''A'' and ''B'' of ''T'' such that ''A'', ''L'' = ''B'', ''L'' (where ''A'', ''L'' is the

reduct In universal algebra and in model theory, a reduct of an algebraic structure is obtained by omitting some of the operations and relations of that structure. The opposite of "reduct" is "expansion." Definition Let ''A'' be an algebraic struc ...

of ''A'' to ''L''), it is the case that ''A'' ⊨ ''φ'' 'a''if and only if ''B'' ⊨ ''φ'' 'a''(for all tuples ''a'' of ''A'') * ''φ'' is equivalent modulo ''T'' to a formula ''ψ'' in ''L''. Less formally: a property is implicitly definable in a theory in language ''L'' (via a formula ''φ'' of an extended language ''L''') only if that property is explicitly definable in that theory (by formula ''ψ'' in the original language ''L''). Clearly the converse holds as well, so that we have an equivalence between implicit and explicit definability. That is, a "property" is explicitly definable with respect to a theory if and only if it is implicitly definable. The theorem does not hold if the condition is restricted to finite models. We may have ''A'' ⊨ ''φ'' 'a''if and only if ''B'' ⊨ ''φ'' 'a''for all pairs ''A'',''B'' of finite models without there being any ''L''-formula ''ψ'' equivalent to ''φ'' modulo ''T''. The result was first proven by

Evert Willem Beth Evert Willem Beth (7 July 1908 – 12 April 1964) was a Dutch philosopher and logician, whose work principally concerned the foundations of mathematics. He was a member of the Significs Group. Biography Beth was born in Almelo, a small ...

Sources

Wilfrid Hodges Wilfrid Augustine Hodges, FBA (born 27 May 1941) is a British mathematician and logician known for his work in model theory. Life Hodges attended New College, Oxford (1959–65), where he received degrees in both '' Literae Humaniores'' and (C ...

''A Shorter Model Theory''. Cambridge University Press, 1997. {{mathlogic-stub Mathematical logic Theorems in the foundations of mathematics