A theorem for classical first-order logic. A theory implicitly defines a non-logical term T if any two models of the theory with the same domain, and the same extensions for other primitive terms, have the same extension for T. Beth's theorem states that a non-logical term T is implicitly defined by the theory if and only if an explicit definition of the term (one giving necessary and sufficient conditions for its application in terms of other primitives) is deducible from the theory. It therefore connects the proof theory of such a logic to its model theory.