 Decidability theorem for propositional logic

There is an algorithm deciding whether any finite propositional formula is a theorem. A formula contains only finitely many atoms, so a finite truth table decides whether it is valid; the completeness theorem for propositional logic identifies validity with provability.

The finite valuation space of propositional logic gives the decision procedure; this theorem is a property of that logic rather than an alternative name for it.