Beth definability

In mathematical logic, Beth definability states that for any two models "A", "B" of a first-order theory "T" in the language L' ⊇ L, if "A"|"L" = "B"|"L" (where "A"|"L" is the reduct of "A" to "L") implies that for all tuples a of "A", "A" ⊨ φ ["a"] if and only if "B" ⊨ φ ["a"] for φ an atomic formula in L', then φ is equivalent modulo "T" to an atomic formula ψ in "L".

Informally this states that implicit definability implies explicit definability. Clearly the converse holds as well, so that we have an equivalence between implicit and explicit definability. That is, a "property" is implicitly definable with respect to a theory if and only if it is explicitly definable. (The definitions of 'implicit definability' and 'explicit definability' should be made precise, but it is fairly clear what is meant by those terms given the statement above of the theorem.)

ources

Hodges W. "A Shorter Model Theory". Cambridge University Press, 1997.