 Principal formula of a type

A principal formula of a type is a logical formula first-order consistent with the base first-order theory that, modulo that first-order theory, implies every logical formula of the partial type. For a complete type it isolates a single point of the type space. A realized finite-tuple partial type in a finite first-order structure has such a logical formula by conjoining one distinguishing logical formula for each competing tuple with a different partial type.