  Suppose that L is a first-order language and M is the first-order language got by adding to L a new predicate symbol R. Suppose also that T is a theory in M. We say that T implicitly defines R if it is false that there are two M-structures which are models of T, have the same elements and interpret all the symbols of L in the same way but interpret the symbol R differently. We say that T defines R explicitly if there is a formula φ(x1,…,xn) of L such that in every model of T, the formulas φ and R(x1,…,xn) are satisfied by exactly the same n-tuples (a1,…,an) of elements. It is easy to see that if T defines R explicitly then it defines R implicitly. (This fact is known as Padoa’s method; Padoa used the failure of implicit definability as a way of proving the failure of explicit definability.) Beth’s theorem is the converse: