Home > Entscheidungsproblem

The question goes back to Gottfried Leibniz, who in the seventeenth century, after having constructed a successful mechanical calculating machine, dreamt of building a machine that could manipulate symbols in order to determine the truth values of mathematical statements. He realized that the first step would have to be a clean formal language, and much of his subsequent work was directed towards that goal. In 1928, David Hilbert and Wilhelm Ackermann posed the question in the form outlined above.

A first-order statement is called “universally valid” or “logically valid” if it follows from the axioms of the first-order predicate calculus. Gödel’s completeness theorem states that a statement is universally valid in this sense if and only if it is true in every interpretation of the formula in a model.

Before the question could be answered, the notion of “algorithm” had to be formally defined. This was done by Alonzo Church in 1936 with the concept of “effective calculability” based on his lambda calculus and by Alan Turing in the same year with his concept of Turing machines. The two approaches are equivalent, an instance of the Church-Turing thesisIn the computability theory the Church-Turing thesis Church's thesis Church's conjecture or Turing's thesis named after Alonzo Church and Alan Turing, is a hypothesis about the nature of mechanical calculation devices, like computers, and what kind of alg.

The negative answer to the Entscheidungsproblem was then given by Alonzo Church in 1936 and independently shortly thereafter by Alan Turing, also in 1936. Church proved that there is no algorithm (defined via recursive functionIn mathematical logic and computer science, the recursive functions are a class of functions from natural numbers to natural numbers which are "computable" in some intuitive sense. In fact, in computability theory it is shown that the recursive functionss) which decides for two given lambda calculus expressions whether they are equivalent or not. He relied heavily on earlier work by Stephen Kleene. Turing reduced the Entscheidungsproblem to the halting problem for Turing machines, and his paper is generally considered to be much more influential than Church’s. The work of both authors was heavily influenced by Kurt GödelKurt Godel [ kurˈt godl ], ( April 28, 1906 January 14, 1978) was a logician, mathematician, and philosopher of mathematics, whose biography lists quite a few nations, although he is usually associated with Austria. He was born in Brunn in Austria-’s earlier work on his incompleteness theoremIn mathematical logic, Godel's incompleteness theorems are two celebrated theorems proved by Kurt Godel in 1930. Somewhat simplified, the first theorem states: In any consistent formalization of mathematics that is sufficiently strong to define the concep, especially by the method of assigning numbers to logical formulas in order to reduce logic to arithmetic.

Turing’s argument follows. Suppose we had a general decision algorithm for first order logic. The question whether a given Turing machine halts or not can be formulated as a first-order statement, which would then be susceptible to the decision algorithm. But Turing had proved earlier that no general algorithm can decide whether a given Turing machine halts.

It is important to realize that if we restrict ourselves to a specific first-order theory with specified object constants, function constants, predicate constants and subject axioms, the truth of statements in that theory may very well be algorithmically decidable. An example of this is given by Presburger arithmeticPresburger arithmetic is the first-order theory of the natural numbers with addition. It is not as powerful as the Peano axioms because multiplication is omitted. In fact, Mojzesz Presburger proved in 1929 that there is an algorithm which decides for any.

However, the general first-order theory of the natural numbers expressed in Peano’s axioms cannot be decided with such an algorithm. This also follows from Turing’s argument given above.