Beth Definability Property

The property that whenever a non-logical symbol (relation, function, or constant) is implicitly definable by a theory — meaning any two models of the theory that agree on the base language also agree on the interpretation of that symbol — then there exists an explicit definition of that symbol by a formula in the original language (i.e., an explicit defining formula).