Suppose T is a theory (i.e., a set of sentences) in a formal language L of logic. A decision procedure for T is a mechanical procedure for calculating whether any given sentence of L is a logical consequence of T. We say that T is decidable if it has a decision procedure and undecidable if not. The decision problem for T is to determine whether or not T is decidable. (One can avoid the slightly vague notion of a mechanical procedure by noting that a theory T is decidable if and only if the set of its.....