Editing Post's theorem (section)

===Higher Turing jumps===

More generally, suppose every set that is recursively enumerable by an oracle machine with an oracle for <math>\emptyset ^{(p)}</math> is in <math>\Sigma^0_{p+1}</math>. Then for an oracle machine with an oracle for <math>\emptyset ^{(p+1)}</math>, <math>\psi^O(m) = \exists m_1: \psi_H(m,m_1)</math> is in <math>\Sigma^0_{p+1}</math>.

Since <math>\psi^O(m)</math> is the same as <math>\varphi(n)</math> for the previous Turing jump, it can be constructed (as we have just done with <math>\varphi(n)</math> above) so that <math>\psi_H(m,m_1)</math> in <math>\Pi^0_p</math>. After moving to prenex formal form the new <math>\varphi(n)</math> is in <math>\Sigma^0_{p+2}</math>.

By induction, every set that is recursively enumerable by an oracle machine with an oracle for <math>\emptyset ^{(p)}</math>, is in <math>\Sigma^0_{p+1}</math>.

'''The other direction''' can be proven by induction as well: Suppose every formula in <math>\Sigma^0_{p+1}</math> can be enumerated by an oracle machine with an oracle for <math>\emptyset ^{(p)}</math>.

Now Suppose <math>\varphi(n)</math> is a formula in <math>\Sigma^0_{p+2}</math> with <math>k_1</math> existential quantifiers followed by <math>k_2</math> universal quantifiers etc. Equivalently, <math>\varphi(n)</math> has <math>k_1</math>> existential quantifiers followed by a negation of a formula in <math>\Sigma^0_{p+1}</math>; the latter formula can be enumerated by an oracle machine with an oracle for <math>\emptyset ^{(p)}</math> and can thus be checked immediately by an oracle for <math>\emptyset ^{(p+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 ^{(p+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.