Model-theoretic definable closure
ID: model-theoretic-definable-closure
For a first-order structure and , the model-theoretic definable closure consists of the elements uniquely specified in by some first-order formula with finitely many parameters from . For example, in a field, the inverse of a nonzero parameter is uniquely defined by , so it belongs to the definable closure of .
Every automorphism of fixing pointwise fixes . The converse uses a sufficiently saturated and strongly homogeneous ambient model with small: if a type over has another realization, homogeneity moves the element, while saturation ensures that failure of unique definability gives another realization. In an arbitrary structure the converse can fail; having few automorphisms does not by itself produce defining formulas. This distinction prevents automorphism rigidity from being confused with definability.
New to topics? Read the docs here!