Editing Computability theory (section)

==Relationships between definability, proof and computability==
There are close relationships between the Turing degree of a set of natural numbers and the difficulty (in terms of the [[arithmetical hierarchy]]) of defining that set using a [[first-order logic|first-order formula]]. One such relationship is made precise by [[Post's theorem]]. A weaker relationship was demonstrated by [[Kurt Gödel]] in the proofs of his [[Gödel's completeness theorem|completeness theorem]] and [[Gödel's incompleteness theorem|incompleteness theorem]]s. Gödel's proofs show that the set of logical consequences of an effective first-order theory is a [[recursively enumerable set|computably enumerable set]], and that if the theory is strong enough this set will be uncomputable. Similarly, [[Tarski's indefinability theorem]] can be interpreted both in terms of definability and in terms of computability.

Computability theory is also linked to [[second-order arithmetic]], a formal theory of natural numbers and sets of natural numbers. The fact that certain sets are computable or relatively computable often implies that these sets can be defined in weak subsystems of second-order arithmetic. The program of [[reverse mathematics]] uses these subsystems to measure the non-computability inherent in well known mathematical theorems. In 1999, Simpson<ref name="Simpson_1999"/> discussed many aspects of second-order arithmetic and reverse mathematics.

The field of [[proof theory]] includes the study of second-order arithmetic and [[Peano arithmetic]], as well as formal theories of the natural numbers weaker than Peano arithmetic. One method of classifying the strength of these weak systems is by characterizing which computable functions the system can prove to be [[total function|total]].<ref name="Fairtlough-Wainer_1998"/> For example, in [[primitive recursive arithmetic]] any computable function that is provably total is actually [[primitive recursive function|primitive recursive]], while [[Peano arithmetic]] proves that functions like the [[Ackermann function]], which are not primitive recursive, are total. Not every total computable function is provably total in Peano arithmetic, however; an example of such a function is provided by [[Goodstein's theorem]].