Editing Mathematical logic (section)

== Recursion theory ==
{{Main|Recursion theory}}
'''[[Recursion theory]]''', also called '''computability theory''', studies the properties of [[computable function]]s and the [[Turing degree]]s, which divide the uncomputable functions into sets that have the same level of uncomputability.  Recursion theory also includes the study of generalized computability and definability.  Recursion theory grew from the work of [[Rózsa Péter]], [[Alonzo Church]] and [[Alan Turing]] in the 1930s, which was greatly extended by [[Stephen Cole Kleene|Kleene]] and [[Emil Leon Post|Post]] in the 1940s.{{sfnp|Soare|2011}}

Classical recursion theory focuses on the computability of functions from the natural numbers to the natural numbers. The fundamental results establish a robust, canonical class of computable functions with numerous independent, equivalent characterizations using [[Turing machine]]s, [[lambda calculus|&lambda; calculus]], and other systems.  More advanced results concern the structure of the Turing degrees and the [[lattice (order)|lattice]] of [[recursively enumerable set]]s.

Generalized recursion theory extends the ideas of recursion theory to computations that are no longer necessarily finite. It includes the study of computability in higher types as well as areas such as [[hyperarithmetical theory]] and [[alpha recursion theory|&alpha;-recursion theory]].

Contemporary research in recursion theory includes the study of applications such as [[algorithmic randomness]], [[computable model theory]], and [[reverse mathematics]], as well as new results in pure recursion theory.

=== 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}}