Entscheidungsproblem
Encyclopedia
In mathematics
, the (ɛntˈʃaɪdʊŋspʁoˌbleːm, German
for 'decision problem
') is a challenge posed by David Hilbert
in 1928. The asks for an algorithm
that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false. Such an algorithm would be able to decide, for example, whether statements such as Goldbach's conjecture
or the Riemann hypothesis
are true, even though no proof or disproof of these statements is known. The has often been identified in particular with the decision problem for first-order logic
(that is, the problem of algorithmically determining whether a first-order statement is universally valid).
In 1936 and 1937 Alonzo Church
and Alan Turing
respectively, published independent papers showing that it is impossible to decide algorithmically whether statements in arithmetic
are true or false, and thus a general solution to the Entscheidungsproblem is impossible. This result is now known as Church's Theorem or the Church–Turing Theorem (not to be confused with the Church–Turing thesis
).
, 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 (Davis 2000: pp. 3–20). 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.
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 " (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).
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 machine
s. It was later recognized that these are equivalent models of computation
.
The negative answer to the was then given by Alonzo Church in 1935–36 and independently
shortly thereafter by Alan Turing in 1936–37. Church proved that there is 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 . 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 is as follows. Suppose we had a general decision algorithm for statements in a first-order
language. 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 proven earlier that no general algorithm can decide whether a given Turing machine halts.
The is related to Hilbert's tenth problem
, which asks for an algorithm
to decide whether Diophantine equation
s have a solution. The non-existence of such an algorithm, established by Yuri Matiyasevich
in 1970, also implies a negative answer to the Entscheidungsproblem.
Some first-order theories are algorithmically decidable; examples of this include Presburger arithmetic
, real closed field
s and static type systems of (most) programming language
s. The general first-order theory of the natural number
s expressed in Peano's axioms
cannot be decided with such an algorithm, however.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, the (ɛntˈʃaɪdʊŋspʁoˌbleːm, German
German language
German is a West Germanic language, related to and classified alongside English and Dutch. With an estimated 90 – 98 million native speakers, German is one of the world's major languages and is the most widely-spoken first language in the European Union....
for 'decision problem
Decision problem
In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...
') is a challenge posed by David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
in 1928. The asks for an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false. Such an algorithm would be able to decide, for example, whether statements such as Goldbach's conjecture
Goldbach's conjecture
Goldbach's conjecture is one of the oldest unsolved problems in number theory and in all of mathematics. It states:A Goldbach number is a number that can be expressed as the sum of two odd primes...
or the Riemann hypothesis
Riemann hypothesis
In mathematics, the Riemann hypothesis, proposed by , is a conjecture about the location of the zeros of the Riemann zeta function which states that all non-trivial zeros have real part 1/2...
are true, even though no proof or disproof of these statements is known. The has often been identified in particular with the decision problem for first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
(that is, the problem of algorithmically determining whether a first-order statement is universally valid).
In 1936 and 1937 Alonzo Church
Alonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
and Alan Turing
Alan Turing
Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...
respectively, published independent papers showing that it is impossible to decide algorithmically whether statements in arithmetic
Arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
are true or false, and thus a general solution to the Entscheidungsproblem is impossible. This result is now known as Church's Theorem or the Church–Turing Theorem (not to be confused with the Church–Turing thesis
Church–Turing thesis
In computability theory, the Church–Turing thesis is a combined hypothesis about the nature of functions whose values are effectively calculable; in more modern terms, algorithmically computable...
).
History of the problem
The origin of the goes back to Gottfried LeibnizGottfried Leibniz
Gottfried Wilhelm Leibniz was a German philosopher and mathematician. He wrote in different languages, primarily in Latin , French and German ....
, who in the seventeenth century, after having constructed a successful mechanical calculating machine
Calculating machine
A calculating machine is a machine designed to come up with calculations or, in other words, computations. One noted machine was the Victorian British scientist Charles Babbage's Difference Engine , designed in the 1840s but never completed in the inventor's lifetime...
, dreamt of building a machine that could manipulate symbols in order to determine the truth values of mathematical statements (Davis 2000: pp. 3–20). He realized that the first step would have to be a clean formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
, and much of his subsequent work was directed towards that goal. In 1928, David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
and Wilhelm Ackermann
Wilhelm Ackermann
Wilhelm Friedrich Ackermann was a German mathematician best known for the Ackermann function, an important example in the theory of computation....
posed the question in the form outlined above.
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 " (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).
Negative answer
Before the question could be answered, the notion of "algorithm" had to be formally defined. This was done by Alonzo ChurchAlonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
in 1936 with the concept of "effective calculability" based on his λ calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
and by Alan Turing in the same year with his concept of Turing machine
Turing machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
s. It was later recognized that these are equivalent models of computation
Model of computation
In computability theory and computational complexity theory, a model of computation is the definition of the set of allowable operations used in computation and their respective costs...
.
The negative answer to the was then given by Alonzo Church in 1935–36 and independently
Multiple discovery
The concept of multiple discovery is the hypothesis that most scientific discoveries and inventions are made independently and more or less simultaneously by multiple scientists and inventors...
shortly thereafter by Alan Turing in 1936–37. Church proved that there is no computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
which decides for two given λ calculus expressions whether they are equivalent or not. He relied heavily on earlier work by Stephen Kleene
Stephen Cole Kleene
Stephen Cole Kleene was an American mathematician who helped lay the foundations for theoretical computer science...
. Turing reduced
Reduction (complexity)
In computability theory and computational complexity theory, a reduction is a transformation of one problem into another problem. Depending on the transformation used this can be used to define complexity classes on a set of problems....
the halting problem
Halting problem
In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
for Turing machines to the . The work of both authors was heavily influenced by Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
'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 is as follows. Suppose we had a general decision algorithm for statements in a first-order
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
language. 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 proven earlier that no general algorithm can decide whether a given Turing machine halts.
The is related to Hilbert's tenth problem
Hilbert's tenth problem
Hilbert's tenth problem is the tenth on the list of Hilbert's problems of 1900. Its statement is as follows:Given a Diophantine equation with any number of unknown quantities and with rational integral numerical coefficients: To devise a process according to which it can be determined in a finite...
, which asks for an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
to decide whether Diophantine equation
Diophantine equation
In mathematics, a Diophantine equation is an indeterminate polynomial equation that allows the variables to be integers only. Diophantine problems have fewer equations than unknown variables and involve finding integers that work correctly for all equations...
s have a solution. The non-existence of such an algorithm, established by Yuri Matiyasevich
Yuri Matiyasevich
Yuri Vladimirovich Matiyasevich, is a Russian mathematician and computer scientist. He is best known for his negative solution of Hilbert's tenth problem, presented in his doctoral thesis, at LOMI .- Biography :* In 1962-1963 studied at Saint Petersburg Lyceum 239...
in 1970, also implies a negative answer to the Entscheidungsproblem.
Some first-order theories are algorithmically decidable; examples of this include Presburger arithmetic
Presburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely...
, real closed field
Real closed field
In mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.-Definitions:...
s and static type systems of (most) programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s. The general first-order theory of the natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s expressed in Peano's axioms
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...
cannot be decided with such an algorithm, however.