The problem of finding an algorithm or decision procedure for deciding whether an arbitrary well-formed formula of a logical system is a theorem of the system. A positive solution is a proof that such a procedure exists; a negative solution is a proof that there can be no such procedure. Truth-tables provide a decision procedure for the propositional calculus, whereas Church's theorem is a negative solution for the first-order predicate calculus with identity.
Philosophy dictionary. Academic. 2011.