Beth definability


In mathematical logic, Beth definability is a result that connects implicit definability of a property to its explicit definability, specifically the theorem states that the two senses of definability are equivalent.

Statement

The theorem states that, given a first-order theory T in the language L' ⊇ L and a formula φ in L', then the following are equivalent:
Less formally: a property is implicitly definable in a theory in language L only if that property is explicitly definable in that theory.
Clearly the converse holds as well, so that we have an equivalence between implicit and explicit definability. That is, a "property" is implicitly definable with respect to a theory if and only if it is explicitly definable.
The theorem does not hold if the condition is restricted to finite models. We may have A ⊨ φ if and only if B ⊨ φ 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.