The Entscheidungsproblem, German for “decision problem,” was posed by David Hilbert and his school in the late 1920s. It asked whether there is a general algorithm that takes any statement of first-order logic and decides whether it is provable. A positive answer would have reduced much of mathematics to mechanical procedure; Hilbert regarded settling it as a central goal of the foundations of mathematics.
In 1936 the question was answered negatively, and independently, by Alonzo Church and Alan Turing. Church published “A note on the Entscheidungsproblem,” using his lambda calculus and the theory of recursive functions, and proved the undecidability of first-order logic. MacTutor notes that this work extended Kurt Godel’s earlier incompleteness results.
Turing reached the same conclusion through his abstract machines, reducing the decision problem to the halting problem for those machines. The Stanford Encyclopedia of Philosophy describes how both demonstrated the decision problem’s unsolvability for first-order logic. Because their two models proved equivalent, the joint result became known as the Church-Turing thesis.
The negative solution to the Entscheidungsproblem is widely seen as the founding moment of computability theory. To prove that no algorithm could exist, Church and Turing first had to define precisely what an algorithm is, and those definitions, the lambda calculus and the Turing machine, became the foundations of theoretical computer science.