= Henkin omission extension lemma
{c}
Let $p(\mathbf x)$ be a <nonprincipal partial type> over a consistent <first-order theory> $T$. Suppose $T\cup\{\sigma(\mathbf c)\}$ is consistent, with $\sigma$ a finite condition in finitely many new constants, and let $\mathbf t(\mathbf c)$ be a tuple of closed terms. Some $\psi\in p$ leaves $T\cup\{\sigma(\mathbf c),\neg\psi(\mathbf t(\mathbf c))\}$ consistent. Otherwise the original-language <first-order formula>
$$
\theta(\mathbf x)=\exists\mathbf z\bigl(\sigma(\mathbf z)\land\mathbf x=\mathbf t(\mathbf z)\bigr)
$$
is consistent with $T$ and entails every member of $p$, contradicting nonprincipality. Replace all new constants occurring in the condition or terms by variables. This lemma makes the omission requirements dense in a countable <Henkin construction>.
Back to article page
