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.