= Extended omitting types theorem for propositional logic
= Propositional omitting types theorem
{synonym}
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.
Back to article page