Propositional type ($\Sigma$)

A propositional type is a collection of propositional formulas to be jointly realized by a Boolean valuation. A valuation realizes it when every member is true and omits it when some member is false. For propositional omission arguments, the collection need not itself be consistent.

If a consistent propositional theory locally omits every member of a countable family of propositional types, it has a Boolean valuation omitting them all. One may also impose any finite condition consistent with the theory. Successively extend the condition by a negated member of the next type; local omission preserves consistency. The propositional compactness theorem then supplies the valuation. Countability of the ambient language and decidability of consistency are not needed for this argument.

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.