Parameter-free definability

A definable set has parameter-free definability when its defining first-order formula uses only the original first-order language, with no additional constants naming elements. Constants already present in the language are allowed. Every such set is invariant under all automorphisms of a first-order structure. For example, zero in the constant-free additive integers is defined by $x+x=x$, while the singleton containing one is not parameter-free definable because negation is an additive automorphism moving it. Invariance is a necessary condition in every structure, and becomes sufficient for finite sets in a countable omega-saturated model.

Every parameter-free definable set is preserved setwise by every automorphism of a first-order structure. For atomic formulas, preservation follows from the definition of a structure automorphism. Logical connectives preserve that equivalence, and a bijection transports existential and universal witnesses in both directions. Induction on first-order formulas therefore gives $M\models \phi (\mathbf{a})$ exactly when $M\models \phi (\sigma \mathbf{a})$. Applied to a defining formula, this proves the displayed equality. With parameters from $B$, restrict to automorphisms fixing $B$ pointwise. An automorphism moving a proposed singleton or taking a proposed function-graph point outside the graph is consequently a direct obstruction to definability.