Principal formula of a type (source code)

= Principal formula of a type
{title2=$T\models\theta(\vec x)\to\phi(\vec x)\quad(\phi\in p)$}

= Principal formulas of a type
{synonym}

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