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. In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer. ... Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics. ... Flowcharts are often used to represent algorithms. ... First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... 1936 (MCMXXXVI) was a leap year starting on Wednesday (link will take you to calendar). ... Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician and logician who was responsible for some of the foundations of theoretical computer science. ... Alan Turing is often considered the father of modern computer science. ... Arithmetic is the current mathematics collaboration of the week! Please help improve it to featured article standard. ...

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. This article or section does not cite its references or sources. ... (16th century - 17th century - 18th century - more centuries) As a means of recording the passage of time, the 17th century was that century which lasted from 1601-1700. ... A calculating machine is a machine designed to come up with calculations (i. ... In mathematics, logic, and computer science, a formal language is a set of finite-length words (i. ... 1928 (MCMXXVIII) was a leap year starting on Sunday (link will take you to calendar). ... David Hilbert (January 23, 1862, Wehlau, East Prussia – February 14, 1943, Göttingen, Germany) was a German mathematician, recognized as one of the most influential mathematicians of the 19th and early 20th centuries. ... Wilhelm Ackermann (March 29, 1896, Herscheid municipality, Germany – December 24, 1962 Lüdenscheid, Germany ) was a German mathematician best known for the Ackermann function, an important example in the theory of computation. ...

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. First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... Gödels completeness theorem is a fundamental theorem in mathematical logic proved by Kurt Gödel in 1929. ...

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 λ 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. Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician and logician who was responsible for some of the foundations of theoretical computer science. ... The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ... An artistic representation of a Turing Machine . ... In computability theory the Church-Turing thesis, Churchs thesis, Churchs conjecture or Turings thesis, named after Alonzo Church and Alan Turing, is a hypothesis about the nature of mechanical calculation devices, such as electronic computers. ...

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 (no computable function) which decides for two given λ 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. It has been suggested that recursive function be merged into this article or section. ... Stephen Cole Kleene (January 5, 1909 - January 25, 1994) was an American mathematician whose work at the University of Wisconsin-Madison helped lay the foundations for theoretical computer science. ... In computability theory the halting problem is a decision problem which can be informally stated as follows: Given a description of a program and its initial input, determine whether the program, when executed on this input, ever halts (completes). ... Kurt Gödel Kurt Gödel (IPA: ) (April 28, 1906 Brno, then Austria-Hungary, now Czech Republic – January 14, 1978 Princeton, New Jersey) was a logician, mathematician, and philosopher of mathematics. ... In mathematical logic, Gödels incompleteness theorems are two celebrated theorems proven by Kurt Gödel in 1931. ... In formal number theory a Gödel numbering is a function which assigns to each symbol and formula of some formal language a unique natural number called a Gödel number (GN). ...

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 has been suggested that Predicate calculus be merged into this article or section. ...

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) Matiyasevichs theorem, proven in 1970 by Yuri Matiyasevich, implies that Hilberts tenth problem is unsolvable. ... Flowcharts are often used to represent algorithms. ... In mathematics, a Diophantine equation is a polynomial equation that only allows the variables to be integers. ... Yuri Matiyasevich born March 2, 1947 in Leningrad, is a Russian mathematician. ... 1970 (MCMLXX) was a common year starting on Thursday (the link is to a full 1970 calendar). ... Matiyasevichs theorem, proven in 1970 by Yuri Matiyasevich, implies that Hilberts tenth problem is unsolvable. ...

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. Presburger arithmetic is the first-order theory of the natural numbers with addition. ... In mathematics, a real closed field is an ordered field F in which any of the following equivalent conditions are true: Every non-negative element of F has a square root in F, and any polynomial of odd degree with coefficients in F has at least one root in F... On computer science, a datatype (often simply type) is a name or label for a set of values and some operations which can be performed on that set of values. ... A programming language is an artificial language that can be used to control the behavior of a machine, particularly a computer. ...

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. Natural number can mean either a positive integer (1, 2, 3, 4, ...) or a non-negative integer (0, 1, 2, 3, 4, ...). Natural numbers have two main purposes: they can be used for counting (there are 3 apples on the table), or they can be used for ordering (this is... In mathematics, the Peano axioms (or Peano postulates) are a set of second-order axioms proposed by Giuseppe Peano which determine the theory of arithmetic. ...

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.

Traditionally, number theory is that branch of pure mathematics concerned with the properties of integers and contains many open problems that are easily understood even by non-mathematicians. ... In mathematics, theoretical computer science and mathematical logic, the computable numbers, also known as the recursive numbers, are the subset of the real numbers consisting of the numbers which can be computed by a finite, terminating algorithm. ... The London Mathematical Society (LMS) is the leading mathematical society in England. ... Martin Davis, (born 1926, New York City) is an American mathematician, known for his work on Hilberts tenth problem. ... Alfred North Whitehead, OM (February 15, 1861 Ramsgate, Kent, England– December 30, 1947 Cambridge, Massachusetts, USA) was an English mathematician who became an American philosopher. ... Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell (May 18, 1872 - February 2, 1970) was one of the most influential mathematicians, philosophers and logicians working mostly in the 20th century. ...

See also

Look up Entscheidungsproblem in
Wiktionary, the free dictionary.

• Halting Problem