Nonprincipal propositional type (source code)

= Nonprincipal propositional type

Relative to a consistent <propositional theory> $T$, a <nonprincipal propositional type> has no formula consistent with $T$ that implies every member modulo $T$. Equivalently, for each finite condition $\theta$ consistent with $T$, some member $\sigma$ leaves $T\cup\{\theta,\neg\sigma\}$ consistent. This is the local omission condition for the <extended omitting types theorem for propositional logic>.