= Solution
An $n$-type over a <first-order theory> $T$ is a <set> of <logical formulas> in the displayed $n$ <free variables> <first-order consistent> with $T$. A <complete type> chooses exactly one of $\phi$ and $\neg\phi$ for each such <logical formula>. Equivalently it is a <maximal consistent> such <set>. For parameter-free <partial types> the <logical formulas> use the original <first-order language>; <partial types> over parameters use additional names for those parameters.
A <partial type> $p(\vec x)$ is principal if some <logical formula> $\theta(\vec x)$ <first-order consistent> with $T$ implies every member of $p$ modulo $T$:
$$
T\models\forall\vec x\,(\theta(\vec x)\to\phi(\vec x))\qquad(\phi\in p).
$$
Such a $\theta$ is a <principal formula of a type> of the <partial type>. For a <complete type> it isolates that <partial type>, so <principal complete types> are exactly <isolated types>.
For a <tuple> $\vec a$ in a <first-order structure> $\mathcal A$, its parameter-free <partial type> is
$$
\boxed{\operatorname{tp}^{\mathcal A}(\vec a)=
\{\phi(\vec x):\mathcal A\models\phi(\vec a)\}.}
$$
It is a <complete type> over $\operatorname{Th}(\mathcal A)$ because the <first-order structure> decides the truth of every <logical formula> at that <tuple>.
Back to article page
