 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.