Entscheidungsproblem (decision problem)

Statement

Hilbert proposed the Entscheidungsproblem: is there an algorithm that, given any first-order logic formula, decides whether it is valid (true in all models)? Turing and Church independently proved it is undecidable. Turing's proof reduced the problem to the halting problem. The result is now axiomatized in computability theory—proved within ZFC, Turing machines formalized as set-theoretic objects.

Formula

First-order validity is undecidable

Equation

VALID(φ) is undecidable (no algorithm decides ∀M: M ⊨ φ)

Proof sketch

Turing showed that if we could decide first-order validity, we could decide the halting problem. Encode a Turing machine M and input x as a first-order formula φ such that φ is valid iff M halts on x. Church proved the same via lambda-definability. Both results appeared in 1936. Proved within ZFC.

Source

Hilbert proposed (1928). Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, 1936. Church, An unsolvable problem of elementary number theory, 1936.

Domains

mathematics, logic