Automorphism invariance of parameter-free definability (source code)

= Automorphism invariance of parameter-free definability
{title2=$\sigma[D]=D$}

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\varphi(\mathbf a)$ exactly when $M\models\varphi(\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.