Textbook of AI

The Entscheidungsproblem (German for "decision problem") was posed by David Hilbert and Wilhelm Ackermann in their 1928 textbook Grundzüge der theoretischen Logik: is there an effective procedure that, given any well-formed statement in first-order logic, decides whether it is provable from a fixed set of axioms? Hilbert hoped the answer would be yes; the dream, central to his formalist programme, was that mathematics could be made fully mechanical.

Hilbert's programme

The Entscheidungsproblem sat within Hilbert's broader 1920s project to place mathematics on completely formal foundations. The programme demanded that mathematics be:

• Complete, every true statement provable from the axioms.
• Consistent, no contradictions derivable.
• Decidable, an algorithm to determine whether any given statement is provable.

Hilbert framed the project in his famous 1900 list and his 1928 ICM address with the slogan "Wir müssen wissen, wir werden wissen" ("We must know, we will know"). The decision problem was the third pillar.

The dismantling: Gödel and then Church-Turing

The programme collapsed in two stages.

First, Kurt Gödel in 1931 proved his incompleteness theorems: any sufficiently powerful consistent formal system contains true statements that cannot be proved within the system, and the system cannot prove its own consistency. This destroyed the completeness leg.

Then, in 1936, the Entscheidungsproblem was answered independently by two mathematicians using two different formalisations of "effective procedure":

• Alonzo Church at Princeton, using the lambda calculus he had developed ("An Unsolvable Problem of Elementary Number Theory", American Journal of Mathematics, 1936).
• Alan Turing in Cambridge, using the Turing machine ("On Computable Numbers, with an Application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, 1936).

Both proved the same result: the Entscheidungsproblem is undecidable. There is no algorithm that, given an arbitrary first-order formula, always halts and correctly reports whether the formula is a theorem. The two proofs proceeded by reducing the problem to the halting problem for their respective models of computation.

The Church-Turing thesis

The agreement between two utterly different formalisations, lambda calculus (functional, manipulating expressions) and Turing machines (mechanical, tape-and-head), led to the Church-Turing thesis: any function "effectively computable" in the intuitive sense is computable by a Turing machine (equivalently, by lambda calculus, by recursive functions, by any of dozens of subsequently proposed models). This is not a theorem but a conjecture about the relationship between intuition and formalism, and it remains universally accepted.

Consequences for AI

The negative answer simultaneously settled Hilbert's question, founded computability theory, and gave AI its mathematical model of what an algorithm is. It also bounded what symbolic AI could achieve: no fully general theorem prover for first-order logic can exist.

Practical theorem provers therefore do one of:

• Exploit decidable fragments: propositional logic (NP-complete but decidable), Presburger arithmetic (additive integers), real closed fields (Tarski-Seidenberg), description logics, the Bernays-Schönfinkel class, the guarded fragment.
• Use semi-decision procedures: resolution, tableaux, superposition. These always terminate when the formula is provable, but may run forever on non-theorems.
• Invoke heuristics that trade completeness for tractability: SAT solvers (CDCL), SMT solvers (Z3, CVC5), model checkers, ATPs (E, Vampire, Spass).
• Use interactive proof assistants (Coq, Lean, Isabelle, Agda) where humans guide the search.

Modern AI returns to the territory in unexpected ways. Lean-RL systems (DeepMind's AlphaProof, OpenAI o-series) train neural networks to guide proof search in formal systems, achieving silver-medal performance on the IMO. The undecidability theorem still stands, no neural network will ever decide first-order logic in finite time on every input, but for any bounded budget of compute, modern theorem provers extract strong performance from the semi-decision regime that Church and Turing left available.