In computability theory

Recursion theory

Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...

 Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy

Arithmetical hierarchy

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...

 and the Turing degree

Turing degree

In computer science and mathematical logic the Turing degree or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set...

s.

Background

The statement of Post's theorem uses several concepts relating to definability and recursion theory. This section gives a brief overview of these concepts, which are covered in depth in their respective articles.

The arithmetical hierarchy

Arithmetical hierarchy

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...

 classifies certain sets of natural numbers that are definable in the language of Peano arithmetic. A formula  is said to be if it is an existential statement in prenex normal form

Prenex normal form

A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers followed by a quantifier-free part .Every formula in classical logic is equivalent to a formula in prenex normal form...

 (all quantifiers at the front) with alternations between existential and universal quantifiers applied to a quantifier free formula. Formally a formula in the language of Peano arithmetic is a formula if it is of the form
where ρ is a quantifier free formula and Q is if m is even and if m is odd. Note that any formula of the form
where contains only bounded quantifier

Bounded quantifier

In the study of formal theories in mathematical logic, bounded quantifiers are often added to a language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and "∃" in that bounded quantifiers restrict the range of the quantified variable...

s is provably equivalent to a formula of the above form from the axioms of Peano arithmetic. Thus it isn't uncommon to see formulas defined in this alternative and technically nonequivalent manner since in practice the distinction is rarely important.

A set of natural numbers A is said to be if it is definable by a formula, that is, if there is a formula such that each number n is in A if and only if holds. It is known that if a set is then it is for any , but for each m there is a set that is not . Thus the number of quantifier alternations required to define a set gives a measure of the complexity of the set.

Post's theorem uses the relativized arithmetical hierarchy as well as the unrelativized hierarchy just defined. A set A of natural numbers is said to be relative to a set B, written , if
A is definable by a formula in an extended language that includes a predicate for membership in B.

While the arithmetical hierarchy measures definability of sets of natural numbers, Turing degrees measure the level of uncomputability of sets of natural numbers. A set A is said to be Turing reducible

Turing reduction

In computability theory, a Turing reduction from a problem A to a problem B, named after Alan Turing, is a reduction which solves A, assuming B is already known . It can be understood as an algorithm that could be used to solve A if it had available to it a subroutine for solving B...

 to a set B, written , if there is an oracle Turing machine that, given an oracle for B, computes the characteristic function of A.
The Turing jump

Turing jump

In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem a successively harder decision problem with the property that is not decidable by an oracle machine with an oracle for .The operator is called a jump...

 of a set A is a form of 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...

 relative to A. Given a set A,
the Turing jump is the set of indices of oracle Turing machines that halt on input 0 when run with oracle A. It is known that every set A is Turing reducible to its Turing jump, but the Turing jump of a set is never Turing reducible to the original set.

Post's theorem uses finitely iterated Turing jumps. For any set A of natural numbers, the notation
indicates the n-fold iterated Turing jump of A. Thus is just A, and is the Turing jump of .

Post's theorem and corollaries

Post's theorem establishes a close connection between the arithmetical hierarchy and the Turing degrees of the form , that is, finitely iterated Turing jumps of the empty set. (The empty set could be replaced with any other computable set without changing the truth of the theorem.)

Post's theorem states:

1. A set B is if and only if is recursively enumerable by an oracle Turing machine with an oracle for , that is, if and only if B is .
2. The set is complete for every . This means that every set is many-one reducible
   Many-one reduction
   In computability theory and computational complexity theory, a many-one reduction is a reduction which converts instances of one decision problem into instances of a second decision problem. Reductions are thus used to measure the relative computational difficulty of two problems.Many-one...
   
   to .

Post's theorem has many corollaries that expose additional relationships between the arithmetical
hierarchy and the Turing degrees. These include:

1. Fix a set C. A set B is if and only if B is . This is the relativization of the first part of Post's theorem to the oracle C.
2. A set B is if and only if . More generally, B is if and only if .
3. A set is defined to be arithmetical if it is for some n. Post's theorem shows that, equivalently, a set is arithmetical if and only if it is Turing reducible to for some m.