= 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.
Back to article page
