Automorphism group of a first-order structure Created 2026-09-28 Updated 2026-10-31
The automorphism group consists of all automorphisms of , with composition as its group operation.
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.
Assume every is finite. Each of its points is isolated: choose, for every other type, a formula separating it from the given one, and conjoin the finitely many choices. Thus every finite tuple in every model has an isolated complete type. Moreover every complete type is realized in every model: its isolating formula is consistent with the complete theory, so the theory entails that the formula has a realization.
For clarity, here is the one-point extension argument needed for both remaining assertions. If tuples and in two models have the same complete type and is any new element in the first, let isolate . The formula belongs to the type of , hence also to that of . Choose with . This extends the tuple map to a partial elementary map. If is different from all earlier entries, the isolating type includes these disequalities, so is new as well.
Apply this argument alternately to the two enumerations of any two countable models. The resulting back-and-forth map is an isomorphism. Thus (ii) implies (i).
Choose any countable model . The same back-and-forth argument, now within , shows that any two tuples of the same complete type are related by an automorphism of a first-order structure. Conversely an automorphism preserves the type. Hence the orbits of on are exactly its complete -types. There are finitely many of them for every , so the automorphism group is an oligomorphic permutation group. Therefore (ii) also implies (iii).
By part (a), the Paris model is well-founded. Let be an automorphism of a first-order structure of . External epsilon induction shows that every element is fixed: if for every , then preservation of membership and extensionality give
Hence is the identity function. This is Paris models are rigid when their complete theory has a well-founded model, so every Paris model of is a rigid first-order structure.
The Ehrenfeucht-Mostowski theorem says that if a first-order theory has an infinite model, then for every total order there is a model generated as the Skolem hull of distinct order indiscernibles , and every order automorphism of extends to an automorphism of .
Given an infinite cardinal , let with the lexicographic order, viewed as consecutive copies of the rational order. In each copy independently choose either the identity or a fixed nonidentity order automorphism of . These choices give distinct order automorphisms of .
Apply the theorem to this order. Distinct order automorphisms act differently on the distinct generators , so their extensions give an injection into the automorphism group of a first-order structure . Therefore , proving that has models with arbitrarily large automorphism groups.
No. The map is an automorphism of a first-order structure for the additive integers, but it sends one to minus one. By automorphism invariance of parameter-free definability, every parameter-free definable singleton is fixed by every structure automorphism. The singleton containing one is not fixed, so it is not definable.