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.