Entscheidungsproblem
   HOME

TheInfoList



OR:

In
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
and
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, the ' (, ) is a challenge posed by
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
and
Wilhelm Ackermann Wilhelm Friedrich Ackermann (; ; 29 March 1896 – 24 December 1962) was a German mathematician and logician best known for his work in mathematical logic and the Ackermann function, an important example in the theory of computation. Biography ...
in 1928. The problem asks for an
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is ''universally valid'', i.e., valid in every
structure A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such as ...
satisfying the axioms.


Completeness theorem

By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the ' can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the
rules of logic In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their Syntax (logic), syntax, and returns a conclusion (or multiple-conclusion logic, ...
. In 1936,
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
and
Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical com ...
published independent papers showing that a general solution to the ' is impossible, assuming that the intuitive notion of "
effectively calculable In logic, mathematics and computer science, especially metalogic and computability theory, an effective method Hunter, Geoffrey, ''Metalogic: An Introduction to the Metatheory of Standard First-Order Logic'', University of California Press, 1971 ...
" is captured by the functions computable by a
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
(or equivalently, by those expressible in the
lambda calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
). This assumption is now known as the
Church–Turing thesis In computability theory, the Church–Turing thesis (also known as computability thesis, the Turing–Church thesis, the Church–Turing conjecture, Church's thesis, Church's conjecture, and Turing's thesis) is a thesis about the nature of comp ...
.


History of the problem

The origin of the goes back to
Gottfried Leibniz Gottfried Wilhelm (von) Leibniz . ( – 14 November 1716) was a German polymath active as a mathematician, philosopher, scientist and diplomat. He is one of the most prominent figures in both the history of philosophy and the history of mathem ...
, who in the seventeenth century, after having constructed a successful mechanical
calculating machine A mechanical calculator, or calculating machine, is a mechanical device used to perform the basic operations of arithmetic automatically, or (historically) a simulation such as an analog computer or a slide rule. Most mechanical calculators wer ...
, dreamt of building a machine that could manipulate symbols in order to determine the
truth value In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values (''true'' or '' false''). Computing In some progr ...
s of mathematical statements. He realized that the first step would have to be a clean
formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of symb ...
, and much of his subsequent work was directed toward that goal. In 1928,
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
and
Wilhelm Ackermann Wilhelm Friedrich Ackermann (; ; 29 March 1896 – 24 December 1962) was a German mathematician and logician best known for his work in mathematical logic and the Ackermann function, an important example in the theory of computation. Biography ...
posed the question in the form outlined above. In continuation of his "program", Hilbert posed three questions at an international conference in 1928, the third of which became known as "Hilbert's ". In 1929,
Moses Schönfinkel Moses Ilyich Schönfinkel (russian: Моисей Исаевич Шейнфинкель, translit=Moisei Isai'evich Sheinfinkel; 29 September 1888 – 1942) was a logician and mathematician, known for the invention of combinatory logic. Life Mose ...
published one paper on special cases of the decision problem, that was prepared by
Paul Bernays Paul Isaac Bernays (17 October 1888 – 18 September 1977) was a Swiss mathematician who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant and close collaborator of ...
. As late as 1930, Hilbert 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 Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
in 1935 with the concept of "effective calculability" based on his
λ-calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation tha ...
, and by Alan Turing the next year with his concept of
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
s. Turing immediately recognized that these are equivalent
models of computation In computer science, and more specifically in computability theory and computational complexity theory, a model of computation is a model which describes how an output of a mathematical function is computed given an input. A model describes how ...
. The negative answer to the was then given by Alonzo Church in 1935–36 (Church's theorem) and independently shortly thereafter by Alan Turing in 1936 (
Turing's proof Turing's proof is a proof by Alan Turing, first published in January 1937 with the title "On Computable Numbers, with an Application to the ". It was the second proof (after Church's theorem) of the negation of Hilbert's ; that is, the conjecture ...
). Church proved that there is no
computable function Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...
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 ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
. Turing reduced the question of the existence of an 'algorithm' or 'general method' able to solve the to the question of the existence of a 'general method' which decides whether any given Turing machine halts or not (the
halting problem In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a g ...
). If 'algorithm' is understood as meaning a method that can be represented as a Turing machine, and with the answer to the latter question negative (in general), the question about the existence of an algorithm for the also must be negative (in general). In his 1936 paper, Turing says: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0". The work of both Church and Turing was heavily influenced by
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imme ...
's earlier work on his
incompleteness theorem Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
, especially by the method of assigning numbers (a
Gödel numbering In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was developed by Kurt Gödel for the proof of his ...
) to logical formulas in order to reduce logic to arithmetic. The ' is related to
Hilbert's tenth problem Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm which, for any given Diophantine equation (a polynomial equat ...
, which asks for an
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
to decide whether
Diophantine equation In mathematics, a Diophantine equation is an equation, typically a polynomial equation in two or more unknowns with integer coefficients, such that the only solutions of interest are the integer ones. A linear Diophantine equation equates to a c ...
s have a solution. The non-existence of such an algorithm, established by the work of
Yuri Matiyasevich Yuri Vladimirovich Matiyasevich, (russian: Ю́рий Влади́мирович Матиясе́вич; born 2 March 1947 in Leningrad) is a Russian mathematician and computer scientist. He is best known for his negative solution of Hilbert's t ...
,
Julia Robinson Julia Hall Bowman Robinson (December 8, 1919July 30, 1985) was an American mathematician noted for her contributions to the fields of computability theory and computational complexity theory—most notably in decision problems. Her work on Hilbe ...
, Martin Davis, and
Hilary Putnam Hilary Whitehall Putnam (; July 31, 1926 – March 13, 2016) was an American philosopher, mathematician, and computer scientist, and a major figure in analytic philosophy in the second half of the 20th century. He made significant contributions ...
, with the final piece of the proof 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 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, omitti ...
,
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. Def ...
s, and static type systems of many
programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...
s. The general first-order theory of the
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called ''Cardinal n ...
s expressed in
Peano's axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
cannot be decided with an algorithm, however.


Practical decision procedures

Having practical decision procedures for classes of logical formulas is of considerable interest for
program verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
and circuit verification. Pure Boolean logical formulas are usually decided using SAT-solving techniques based on the
DPLL algorithm In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solvi ...
. Conjunctive formulas over linear real or rational arithmetic can be decided using the
simplex algorithm In mathematical optimization, Dantzig's simplex algorithm (or simplex method) is a popular algorithm for linear programming. The name of the algorithm is derived from the concept of a simplex and was suggested by T. S. Motzkin. Simplices are n ...
, formulas in linear integer 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, omitti ...
) can be decided using
Cooper's algorithm Cooper, Cooper's, Coopers and similar may refer to: * Cooper (profession), a maker of wooden casks and other staved vessels Arts and entertainment * Cooper (producers), alias of Dutch producers Klubbheads * Cooper (video game character), in ' ...
or William Pugh's
Omega test Omega (; capital: Ω, lowercase: ω; Ancient Greek ὦ, later ὦ μέγα, Modern Greek ωμέγα) is the twenty-fourth and final letter in the Greek alphabet. In the Greek numeric system/isopsephy (gematria), it has a value of 800. The wo ...
. Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using SMT-solving techniques, which combine SAT-solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of
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. Def ...
s, is decidable; this is the
Tarski–Seidenberg theorem In mathematics, the Tarski–Seidenberg theorem states that a set in (''n'' + 1)-dimensional space defined by polynomial equations and inequalities can be projected down onto ''n''-dimensional space, and the resulting set is still defina ...
, which has been implemented in computers by using the
cylindrical algebraic decomposition In mathematics, cylindrical algebraic decomposition (CAD) is a notion, and an algorithm to compute it, that are fundamental for computer algebra and real algebraic geometry. Given a set ''S'' of polynomials in R''n'', a cylindrical algebraic decom ...
.


See also

*
Automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...
*
Decidability (logic) In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems ar ...
*
Hilbert's second problem In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his Hilbert's problems, 23 problems. It asks for a proof that the arithmetic is consistency proof, consistent – free of any internal contradictions. Hilber ...
*
Oracle machine In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to solve certain problems in a s ...
*
Turing's proof Turing's proof is a proof by Alan Turing, first published in January 1937 with the title "On Computable Numbers, with an Application to the ". It was the second proof (after Church's theorem) of the negation of Hilbert's ; that is, the conjecture ...


Notes


References

*
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many a ...
and
Wilhelm Ackermann Wilhelm Friedrich Ackermann (; ; 29 March 1896 – 24 December 1962) was a German mathematician and logician best known for his work in mathematical logic and the Ackermann function, an important example in the theory of computation. Biography ...
(1928). ''Grundzüge der theoretischen Logik'' (''Principles of Mathematical Logic''). Springer-Verlag, . *
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
, "An unsolvable problem of
elementary number theory Number theory (or arithmetic or higher arithmetic in older usage) is a branch of pure mathematics devoted primarily to the study of the integers and integer-valued functions. German mathematician Carl Friedrich Gauss (1777–1855) said, "Math ...
", American Journal of Mathematics, 58 (1936), pp 345–363 *
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
, "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), pp 40–41. * Martin Davis, 2000, ''Engines of Logic'', W.W. Norton & Company, London, pbk. *
Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical com ...
, "
On Computable Numbers, with an Application to the Entscheidungsproblem Turing's proof is a proof by Alan Turing, first published in January 1937 with the title "On Computable Numbers, with an Application to the ". It was the second proof (after Church's theorem) of the negation of Hilbert's ; that is, the conjecture ...
", Proceedings of the
London Mathematical Society The London Mathematical Society (LMS) is one of the United Kingdom's learned societies for mathematics (the others being the Royal Statistical Society (RSS), the Institute of Mathematics and its Applications (IMA), the Edinburgh Mathematical S ...
, Series 2, 42 (1936–7), pp 230–265. Online versions
from journal websitefrom Turing Digital Archivefrom abelard.org
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 Gödel, Church, Rosser, Kleene, and Post. *
Andrew Hodges Andrew Philip Hodges (; born 1949) is a British mathematician, author and emeritus senior research fellow at Wadham College, Oxford. Education Hodges was born in London in 1949 and educated at Birkbeck, University of London where he was award ...
, Alan Turing: The Enigma,
Simon and Schuster Simon & Schuster () is an American publishing company and a subsidiary of Paramount Global. It was founded in New York City on January 2, 1924 by Richard L. Simon and M. Lincoln Schuster. As of 2016, Simon & Schuster was the third largest publ ...
, New York, 1983. Alan M. Turing's biography. Cf Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof. *
Robert Soare Robert Irving Soare is an American mathematician. He is the Paul Snowden Russell Distinguished Service Professor of Mathematics and Computer Science at the University of Chicago, where he has been on the faculty since 1967. He proved, together wi ...
, "Computability and recursion", Bull. Symbolic Logic 2 (1996), no. 3, 284–321. * Stephen Toulmin, "Fall of a Genius", a book review of " Alan Turing: The Enigma by Andrew Hodges", in The New York Review of Books, 19 January 1984, p. 3ff. *
Alfred North Whitehead Alfred North Whitehead (15 February 1861 – 30 December 1947) was an English mathematician and philosopher. He is best known as the defining figure of the philosophical school known as process philosophy, which today has found applicat ...
and
Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
, 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.


External links

* {{Metalogic Theory of computation Computability theory Gottfried Wilhelm Leibniz Mathematical logic Metatheorems Undecidable problems