Principal complete type
= Principal complete type
A <principal complete type> is isolated by one <first-order consistent> <first-order formula>: modulo the <first-order theory>, that <logical formula> implies every member of the <partial type>. For <complete types> this is exactly an <isolated type>. The qualifier complete distinguishes this notion from <partial types>.