Algebraic type (source code)

= Algebraic type

A complete type is algebraic when it contains a formula having finitely many realizations in a model of the theory. A one-element example is the type containing $x=c$ for a named constant. Such a type cannot gain infinitely many realizations in an <elementarily equivalent> structure. An <isolated type> need not be algebraic: the unique empty-set one-type in a <dense linear order without endpoints> is isolated by $x=x$ and has infinitely many realizations.