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