Entscheidungsproblem
From Free net encyclopedia
The Entscheidungsproblem (German for 'decision problem') is the challenge in symbolic logic to find a general algorithm which decides for given first-order statements whether they are universally valid or not. In 1936, working independently, Alonzo Church and Alan Turing both showed that this is impossible. As a consequence, it is in particular impossible to decide algorithmically whether statements in arithmetic are true or false.
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.
In continuation of his "program" with which he challenged the mathematics community in 1900, at a 1928 international conference David Hilbert asked three questions, the third of which became known as "Hilbert's Entscheidungsproblem" [Hodges p. 91]. As late as 1930 he believed that there would be no such thing as an unsolvable problem (Hodges p. 92, quoting from Hilbert).
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 thesis.
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 functions) 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 halting problem for Turing machines to the Entscheidungsproblem, 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ödel's earlier work on his incompleteness theorem, especially by the method of assigning numbers (a Gödel numbering) 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.
The Entscheidungsproblem is related to Hilbert's tenth problem, which asks for an algorithm to decide whether Diophantine equations have a solution. The non-existence of such an algorithm (proven by Yuri Matiyasevich in 1970) implies a negative answer to the Entscheidungsproblem. (see Matiyasevich's theorem)
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. Examples of this include Presburger arithmetic, real closed fields and static type systems of programming languages.
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.
References
- Alonzo Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, 58 (1936), pp 345 - 363
- Alonzo Church, "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), pp 40 - 41.
- Alan Turing, "On computable numbers, with an application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp 230 - 265. Online version. Errata appeared in Series 2, 43 (1937), pp 544 - 546.
- Martin Davis, "The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions", Raven Press, New York, 1965. Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.
- Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York, 1983. Allen M. Turing's biography. Cf Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
- Stephen Toulmin, "Fall of a Genius", a book review of "Alan Turing: The Enigma by Andrew Hodges", in The New York Review of Books, January 19, 1984, p. 3ff.
- Alfred North Whitehead and Bertrand Russel, Principia Mathematica to *56, Cambridge at the University Press, 1962. Re: the problem of paradoxes, the authors discuss the problem of a set not be an object in any of its "determining functions", in particular "Introduction, Chap. 1 p. 24 "...difficulties which arise in formal logic", and Chap. 2.I. "The Vicious-Circle Principle" p.37ff, and Chap. 2.VIII. "The Contradictions" p.60 ff.
See also
es:Entscheidungsproblem fr:Problème de la décision pt:Entscheidungsproblem