In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.
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 classifies certain sets of natural numbers that are definable in the language of Peano arithmetic.
if it is an existential statement in prenex normal form (all quantifiers at the front) with
formula in an extended language that includes a predicate for membership in
While the arithmetical hierarchy measures definability of sets of natural numbers, Turing degrees measure the level of uncomputability of sets of natural numbers.
is the set of indices of oracle Turing machines that halt on input
Post's theorem uses finitely iterated Turing jumps.
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.
Post's theorem states: Post's theorem has many corollaries that expose additional relationships between the arithmetical hierarchy and the Turing degrees.
The exact relation depends on the specific implementation of the notion of Turing machine (e.g. their alphabet, allowed mode of motion along the tape, etc.)
For example, for a prefix-free Turing machine with binary alphabet and no blank symbol, we may use the following notations: For a prefix-free Turing machine we may use, for input n, the initial tape configuration
steps can thus be written as the conjunction of the initial conditions and the following formulas, quantified over
is satisfied, where: This is a first-order arithmetic formula with no unbounded quantifiers, i.e. it is in
be a set that can be recursively enumerated by a Turing machine.
This can be formalized by the first-order arithmetical formula presented above.
–tuples of natural numbers and run a Turing machine that goes through all of them until it finds the formula is satisfied.
This Turing machine halts on precisely the set of natural numbers satisfying
Suppose the decision problem itself can be formalized by a first-order arithmetic formula
Moving to prenex normal form, we get that the oracle machine halts on input
by a single number - their maximum - without changing the truth value of
For the oracle to the halting problem over Turing machines,
> existential quantifiers followed by a negation of a formula in
; the latter formula can be enumerated by a Turing machine and can thus be checked immediately by an oracle for
This oracle machine halts on precisely the set of natural numbers satisfying
The other direction can be proven by induction as well: Suppose every formula in
This oracle machine halts on precisely the set of natural numbers satisfying
Rogers, H. The Theory of Recursive Functions and Effective Computability, MIT Press.