Nonprincipal complete type
= Nonprincipal complete type
A <nonprincipal complete type> has no <first-order consistent> <first-order formula> implying all its members. In a complete <countable> <first-order theory> such a <partial type> can be omitted in a <countable> <first-order model> by the <omitting types theorem>. A <partial type> realized by a parameter-free definable <tuple> is principal.