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 exactly when . Applied to a defining formula, this proves the displayed equality. With parameters from , restrict to automorphisms fixing pointwise. An automorphism moving a proposed singleton or taking a proposed function-graph point outside the graph is consequently a direct obstruction to definability.
Articles by others on the same topic
There are currently no matching articles.