Editing Mathematical logic (section)

=== Algorithmically unsolvable problems ===
An important subfield of recursion theory studies algorithmic unsolvability; a [[decision problem]] or [[function problem]] is '''algorithmically unsolvable''' if there is no possible computable algorithm that returns the correct answer for all legal inputs to the problem. The first results about unsolvability, obtained independently by Church and Turing in 1936, showed that the [[Entscheidungsproblem]] is algorithmically unsolvable. Turing proved this by establishing the unsolvability of the [[halting problem]], a result with far-ranging implications in both recursion theory and computer science.

There are many known examples of undecidable problems from ordinary mathematics. The [[word problem for groups]] was proved algorithmically unsolvable by [[Pyotr Novikov]] in 1955 and independently by W. Boone in 1959.  The [[busy beaver]] problem, developed by [[Tibor Radó]] in 1962, is another well-known example.

[[Hilbert's tenth problem]] asked for an algorithm to determine whether a multivariate polynomial equation with integer coefficients has a solution in the integers. Partial progress was made by [[Julia Robinson]], [[Martin Davis (mathematician)|Martin Davis]] and [[Hilary Putnam]]. The algorithmic unsolvability of the problem was proved by [[Yuri Matiyasevich]] in 1970.{{sfnp|Davis|1973}}