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