Let be a finite set and . Then there’s an algorithm that can determine, in finite time, whether .

Proof

Trivial if is replaced with by Completeness Theorem. Just do a truth table for of all possible values of the primitive propositions that occur in where is the number of such propositions.