Parameter-free definability (source code)

= 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>.