Post's theorem
In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees. 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 classifies certain sets of natural numbers that are definable in the language of Peano arithmetic. A formula is said to be formula_1 if it is an existential statement in prenex normal form (all quantifiers at the front) with formula_2  alternations between existential and universal quantifiers applied to a formula with bounded quantifiers only. Formally a formula formula_3 in the language of Peano arithmetic is a formula_1 formula if it is of the form where formula_6 contains only bounded quantifiers and "Q" is formula_7 if "m" is even and formula_8 if "m" is odd. A set of natural numbers formula_9 is said to be formula_10 if it is definable by a formula_10 formula, that is, if there is a formula_10 formula formula_3 such that each number formula_14 is in formula_9 if and only if formula_16 holds. It is known that  if a set is formula_10 then it is formula_18 for any formula_19, but for each "m" there is a formula_20 set that is not formula_10. 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 formula_9 of natural numbers is said to be formula_10 relative to a set formula_24, written formula_25, if formula_9 is definable by a formula_10 formula in an extended language that includes a predicate for membership in formula_24. 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 formula_9 is said to be Turing reducible to a set formula_24, written formula_31, if there is an oracle Turing machine that, given an oracle for formula_24, computes the characteristic function of formula_9. The Turing jump of a set formula_9 is a form of the Halting problem relative to formula_9. Given a set formula_9, the Turing jump formula_37 is the set of indices of oracle Turing machines that halt on input formula_38 when run with oracle formula_9 . It is known that every set formula_9 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 formula_9 of natural numbers, the notation formula_42 indicates the formula_14–fold iterated Turing jump of formula_9. Thus formula_45 is just formula_9, and formula_47 is the Turing jump of formula_42. Post's theorem and corollaries. Post's theorem establishes a close connection between the arithmetical hierarchy and the Turing degrees of the form formula_49, 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: Post's theorem has many corollaries that expose additional relationships between the arithmetical hierarchy and the Turing degrees. These include: Proof of Post's theorem. Formalization of Turing machines in first-order arithmetic. The operation of a Turing machine formula_76 on input formula_14 can be formalized logically in first-order arithmetic. For example, we may use symbols formula_78, formula_79, and formula_80 for the tape configuration, machine state and location along the tape after formula_81 steps , respectively. formula_76's transition system determines the relation between formula_83 and formula_84; their initial values (for formula_85) are the input, the initial state and zero, respectively. The machine halts if and only if there is a number formula_81 such that formula_79 is the halting state. 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.) In case formula_76 halts at time formula_89, the relation between formula_83 and formula_84 must be satisfied only for k bounded from above by formula_89. Thus there is a formula formula_93  in first-order arithmetic with no unbounded quantifiers, such that formula_76 halts on input formula_14 at time formula_89 at most if and only if formula_93 is satisfied. Implementation example. 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 formula_110 where cat stands for concatenation; thus formula_111 is a formula_112length string of formula_113 followed by formula_38 and then by formula_14. The operation of the Turing machine at the first formula_89 steps can thus  be written as the conjunction of the initial conditions and the following formulas, quantified over formula_81 for all formula_118: T halts on input formula_14 at time formula_89 at most if and only if formula_93 is satisfied, where: This is a first-order arithmetic formula with no unbounded quantifiers, i.e. it is in formula_130. Recursively enumerable sets. Let formula_131 be a set that can be recursively enumerated by a Turing machine. Then there is a Turing machine formula_76 that for every formula_14 in formula_131, formula_76 halts when given formula_14 as an input. This can be formalized by the first-order arithmetical  formula presented above. The members of formula_131 are the numbers formula_14 satisfying the following formula: formula_139 This formula is in formula_140. Therefore, formula_131 is in formula_140. Thus every recursively enumerable set is in formula_140. The converse is true as well: for every formula formula_144 in formula_140 with k existential quantifiers, we may enumerate the formula_81–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 formula_144, and thus enumerates its corresponding set. Oracle machines. Similarly, the  operation of an oracle machine formula_76 with an oracle O that halts after at most formula_89 steps on input formula_14 can be described by a first-order formula formula_151, except that the formula formula_152 now includes: If the oracle is for a decision problem, formula_153 is always "Yes" or "No", which we may formalize as 0 or 1. Suppose the decision problem itself can be formalized by a first-order arithmetic formula formula_159. Then formula_76 halts on formula_14 after at most formula_89 steps if and only if the following formula is satisfied: formula_163 where formula_164 is a first-order formula  with no unbounded quantifiers. Turing jump. If O is an oracle to the halting problem of a machine formula_165, then formula_159 is the same as "there exists formula_167 such that formula_165 starting with input m is at the halting state after formula_167 steps". Thus: formula_170 where formula_171 is a first-order formula that formalizes formula_165. If formula_165 is a Turing machine (with no oracle), formula_171 is in formula_175 (i.e. it has no unbounded quantifiers). Since there is a finite number of numbers m satisfying formula_157, we may choose the same number of steps for all of them: there is a  number formula_167, such that formula_165 halts after formula_167 steps precisely on those inputs formula_157 for which it halts at all. Moving to prenex normal form, we get that the oracle machine halts on input formula_14 if and only if the following formula is satisfied: formula_182 (informally, there is a "maximal number of steps"formula_167 such every oracle that does not halt within the first formula_167 steps does not stop at all; however, for everyformula_185, each oracle that halts after formula_185 steps does halt). Note that we may replace both formula_89 and formula_167 by a single number - their maximum - without changing the  truth value of formula_144. Thus we may write: formula_190 For the oracle to the halting problem over Turing machines, formula_171 is in formula_192 and formula_144 is in formula_194. Thus every set that is recursively enumerable by an oracle machine with an oracle for formula_195, is in formula_194. The converse is true as well: Suppose formula_144 is a formula in formula_194 with formula_199 existential quantifiers followed by formula_200 universal quantifiers. Equivalently, formula_144 has formula_199> existential quantifiers followed by a negation of a formula in formula_140; the latter formula can be enumerated by a Turing machine and can thus be checked  immediately by an oracle for formula_195. We may thus enumerate the formula_199–tuples of natural numbers and run an oracle machine with an oracle for formula_195 that goes through all of them until it finds a satisfaction for the formula. This oracle machine halts on precisely the set of natural numbers satisfying formula_144, and thus enumerates its corresponding set. Higher Turing jumps. More generally, suppose every set that is recursively enumerable by an oracle machine with an oracle for formula_208 is in formula_209. Then for an oracle machine with an oracle for formula_210, formula_170 is in formula_209. Since formula_159 is  the same as formula_144 for the previous Turing jump, it can be constructed (as we have just done with formula_144 above) so that formula_171 in formula_217. After moving to prenex formal form the new formula_144 is in formula_219. By induction, every set that is recursively enumerable by an oracle machine with an oracle for formula_208, is in formula_209. The other direction can be proven by induction as well: Suppose every formula in formula_209 can be enumerated by an oracle machine with an oracle for formula_208. Now Suppose formula_144 is a formula in formula_219 with formula_199 existential quantifiers followed by formula_200  universal quantifiers etc. Equivalently, formula_144 has formula_199> existential quantifiers followed by a negation of a formula in formula_209; the latter formula can be enumerated by an oracle machine with an oracle for formula_208 and can thus be checked immediately by an oracle for formula_210. We may thus enumerate the formula_199–tuples of natural numbers and run an oracle machine with an oracle for formula_210 that goes through all of them until it finds a satisfaction for the formula. This oracle machine halts on precisely the set of natural numbers satisfying formula_144, and thus enumerates its corresponding set. References. Rogers , H. "The Theory of Recursive Functions and Effective Computability", MIT Press. ; Soare, R. "Recursively enumerable sets and degrees." Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1987.