Pointwise definable model (source code)

= Pointwise definable model

= Pointwise definable
{synonym}

Every element of a pointwise definable model is uniquely specified by a formula with no added parameters. Finite tuples are then uniquely specified by conjunctions of their defining formulas. For a <complete theory> these formulas isolate the tuple types, so such a model is an <atomic model>. The converse fails: a <countable> <dense linear order without endpoints> with a named point is atomic, while its other points are moved by <structure automorphisms> fixing that point.