Principal partial type (source code)

= Principal partial type

A <partial type> $p(\mathbf x)$ is principal over $T$ if some formula $\theta(\mathbf x)$ with $T\cup\{\exists\mathbf x\,\theta\}$ consistent implies each formula of $p$ modulo $T$. For complete types this is the usual notion of an <isolated type>. For an incomplete type, the isolating formula need not belong to the type itself.