Editing Post's theorem (section)

===Turing jump===

If O is an oracle to the halting problem of a machine <math>T'</math>, then <math>\psi^O(m)</math> is the same as "there exists <math>m_1</math> such that <math>T'</math> starting with input m is at the halting state after <math>m_1</math> steps". 
Thus:
<math>\psi^O(m) = \exists m_1: \psi_H(m,m_1)</math>
where <math>\psi_H(m,m_1)</math> is a first-order formula that formalizes <math>T'</math>. If <math>T'</math> is a Turing machine (with no oracle), <math>\psi_H(m,m_1)</math> is in <math>\Sigma^0_0 = \Pi^0_0</math> (i.e. it has no unbounded quantifiers).

Since there is a finite number of numbers m satisfying <math>m<2^{n_1}</math>, we may choose the same number of steps for all of them: there is a number <math>m_1</math>, such that <math>T'</math> halts after <math>m_1</math> steps precisely on those inputs <math>m<2^{n_1}</math> for which it halts at all.

Moving to [[prenex normal form]], we get that the oracle machine halts on input <math>n</math> if and only if the following formula is satisfied:
<math>\varphi(n) =\exists n_1\exists m_1 \forall m_2 :(\psi_H(m,m_2)\rightarrow (O_m=1)) \land(\lnot\psi_H(m,m_1)\rightarrow (O_m=0))) \land {\varphi_O}_1(n,n_1)</math>

(informally, there is a "maximal number of steps"<math>m_1</math> such every oracle that does not halt within the first <math>m_1</math> steps does not stop at all; however, for every<math>m_2</math>, each oracle that halts after <math>m_2</math> steps does halt).

Note that we may replace both <math>n_1</math> and <math>m_1</math> by a single number - their maximum - without changing the truth value of <math>\varphi(n)</math>. Thus we may write:
<math>\varphi(n) =\exists n_1 \forall m_2 :(\psi_H(m,m_2)\rightarrow (O_m=1)) \land(\lnot\psi_H(m,n_1)\rightarrow (O_m=0))) \land {\varphi_O}_1(n,n_1)</math>

For the oracle to the halting problem over Turing machines, <math>\psi_H(m,m_1)</math> is in <math>\Pi^0_0</math> and <math>\varphi(n)</math> is in <math>\Sigma^0_2</math>. Thus every set that is recursively enumerable by an oracle machine with an oracle for <math>\emptyset ^{(1)}</math>, is in <math>\Sigma^0_2</math>.

The converse is true as well: Suppose <math>\varphi(n)</math> is a formula in <math>\Sigma^0_2</math> with <math>k_1</math> existential quantifiers followed by <math>k_2</math> universal quantifiers. Equivalently, <math>\varphi(n)</math> has <math>k_1</math>> existential quantifiers followed by a negation of a formula in <math>\Sigma^0_1</math>; the latter formula can be enumerated by a Turing machine and can thus be checked immediately by an oracle for <math>\emptyset ^{(1)}</math>.

We may thus enumerate the <math>k_1</math>&ndash;tuples of natural numbers and run an oracle machine with an oracle for <math>\emptyset ^{(1)}</math> 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 <math>\varphi(n)</math>, and thus enumerates its corresponding set.