Model-theoretic definable closure (source code)

= Model-theoretic definable closure
{title2=$\operatorname{dcl}(A)$}

An element belongs to $\operatorname{dcl}(A)$ when it is the unique realization of some formula with parameters from $A$. Equivalently, it is fixed by every automorphism fixing $A$ pointwise.