Textbook of AI

A decision problem -- a question with a yes/no answer applied to a class of instances -- is decidable (or recursive) if there exists an algorithm, equivalently a Turing machine, that always halts and returns the correct yes-or-no answer for every instance. A problem is undecidable if no such algorithm exists. Decidability is the boundary between what can in principle be automated and what cannot.

The class of decidable problems sits inside the larger class of semi-decidable (also called recursively enumerable or r.e.) problems, for which an algorithm exists that halts with "yes" whenever the answer is yes, but may run forever when the answer is no. Equivalently, the set of yes-instances is the range of some computable function. Symmetrically, co-r.e. problems are those whose no-instances can be enumerated. A problem is decidable iff it is both r.e. and co-r.e.

The canonical undecidable problem is the halting problem: given the description of a Turing machine $M$ and an input $w$, does $M$ halt on $w$? Turing's 1936 proof by diagonalisation shows no algorithm can decide this; the halting problem is r.e. (run $M$ on $w$ for ever-longer times -- if it halts, answer yes) but not co-r.e. Rice's theorem strengthens this: every non-trivial semantic property of computable functions is undecidable. Reductions from the halting problem then establish undecidability of program equivalence, the Post correspondence problem, Hilbert's tenth problem (Diophantine equations, Matiyasevich 1970), the word problem for groups (Novikov, Boone), tiling problems and many more.

Decidability boundaries shape what symbolic AI can automate:

• Propositional logic is decidable (in NP, conjectured not in P; the SAT problem).
• First-order logic is undecidable (Church 1936, Turing 1936) but semi-decidable: a sound and complete proof procedure exists (resolution, tableaux), but it may not terminate on non-theorems.
• Higher-order logic and set theory (ZFC) are not even semi-decidable in general.
• Linear arithmetic over the integers (Presburger arithmetic) is decidable, although triple-exponential in worst case.
• Arithmetic with multiplication (Peano arithmetic) is undecidable, by Gödel's incompleteness theorems combined with Church--Turing.
• Real closed fields (Tarski 1948) are decidable -- Tarski's quantifier elimination algorithm.
• Description logics sit on a carefully designed decidable fragment of first-order logic, which is why ontologies (OWL, semantic web) can be reasoned over.

Modern theorem provers, SMT solvers and model checkers exploit decidable theories (linear arithmetic, bit-vectors, arrays, strings, uninterpreted functions) and combine them with heuristic methods for the undecidable parts. The DPLL(T) framework underlying Z3, CVC5 and others integrates SAT solving with theory-specific decision procedures via the Nelson--Oppen combination method.

Historically, David Hilbert's Entscheidungsproblem (1928) asked whether a single procedure could decide any first-order statement. Alonzo Church's lambda calculus and Alan Turing's Turing machine, both in 1936, gave equivalent negative answers, simultaneously founding computability theory and the theoretical basis of computer science. Together with Gödel's incompleteness theorems (1931), these results bound the reach of every symbolic AI system that has ever been built and motivate the empirical, statistical character of modern machine learning.