Entscheidungsproblem

The Entscheidungsproblem (also known as the decision problem) is a challenge posed by David Hilbert in 1928. The Entscheidungsproblem asks for an algorithm that takes as input a statement of a first-order logic (possibly with a finite number of axioms beyond the usual axioms of first-order logic) and answers “Yes” or “No” according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms. By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic.

In 1936, Alonzo Church and Alan Turing published independent papers showing that a general solution to the Entscheidungsproblem is impossible, assuming that the intuitive notion of “effectively calculable” is captured by the functions computable by a Turing machine (or equivalently, by those expressible in the lambda calculus). This assumption is now known as the Church-Turing thesis.

It had strong importance in the modern mathematics and we can say that modern algorithmics and a partial formalization of algorithm concepts started with the attempts to solve the Entscheidungsproblem.

See also

Artificial Intelligence, Computer Complexity, Turing Machines, Automata theory, Theory of computation, Algorithmics

Papers

• Turing, Alan M. (1936-37). On Computable Numbers, With An Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, Series 2 42: 230-265.
• Church, Alonzo (1936b). A Note on the Entscheidungsproblem. The Journal of Symbolic Logic 1 (1): 40-41.
• Alonzo Church, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp 345–363