First-order logic has the Beth definability property.
For first-order logic, the theorem states that, given a 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 (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.
The theorem does not hold if the condition is restricted to finite models.
This mathematical logic-related article is a stub.