. Theories, in the sense in which arithmetic is a theory, are decidable if formalizations exist for them which are COMPLETE. In systems without CONTINGENT propositions, such as formalizations of arithmetic, a well-formed formula (see AXIOM SYSTEM) is decidable if and only if it or its negation is a theorem. Where contingent propositions enter, as in formalizations of the propositional CALCULUS, a well-formed formula is decidable if and only if one can prove whether it is logically true, logically false, or neither. A decision procedure (one kind of ALGORITHM) lets one decide this mechanically by simply following a rule in finitely many steps.
Decision procedures exist for the propositional and monadic predicate CALCULI, but not, in general, for more complex systems. Proof that such a procedure exists, or does not exist, for a given sphere is called a positive or negative solution, respectively, to the decision problem. The negative solution for the predicate calculus (beyond the monadic) is Church’s theorem (1936).
