Post's theorem

In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.

BackgroundEdit

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   if it is an existential statement in prenex normal form (all quantifiers at the front) with   alternations between existential and universal quantifiers applied to a formula with bounded quantifiers only. Formally a formula   in the language of Peano arithmetic is a   formula if it is of the form

 

where   contains only bounded quantifiers and Q is   if m is even and   if m is odd.

A set of natural numbers   is said to be   if it is definable by a   formula, that is, if there is a   formula   such that each number   is in   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   of natural numbers is said to be   relative to a set  , written  , if   is definable by a   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. A set   is said to be Turing reducible to a set  , written  , if there is an oracle Turing machine that, given an oracle for  , computes the characteristic function of  . The Turing jump of a set   is a form of the Halting problem relative to  . Given a set  , the Turing jump   is the set of indices of oracle Turing machines that halt on input   when run with oracle  . It is known that every set   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   of natural numbers, the notation   indicates the  –fold iterated Turing jump of  . Thus   is just  , and   is the Turing jump of  .

Post's theorem and corollariesEdit

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   is   if and only if   is recursively enumerable by an oracle Turing machine with an oracle for  , that is, if and only if   is  .
  2. The set   is  -complete for every  . This means that every   set is many-one reducible 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  . A set   is   if and only if   is  . This is the relativization of the first part of Post's theorem to the oracle  .
  2. A set   is   if and only if  . More generally,   is   if and only if  .
  3. A set is defined to be arithmetical if it is   for some  . Post's theorem shows that, equivalently, a set is arithmetical if and only if it is Turing reducible to   for some m.

Proof of Post's theoremEdit

Formalization of Turing machines in first-order arithmeticEdit

The operation of a Turing machine   on input   can be formalized logically in first-order arithmetic. For example, we may use symbols  ,  , and   for the tape configuration, machine state and location along the tape after   steps, respectively.  's transition system determines the relation between   and  ; their initial values (for  ) are the input, the initial state and zero, respectively. The machine halts if and only if there is a number   such that   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   halts at time  , the relation between   and   must be satisfied only for k bounded from above by  .

Thus there is a formula   in first-order arithmetic with no unbounded quantifiers, such that   halts on input   at time   at most if and only if   is satisfied.

Implementation exampleEdit

For example, for a prefix-free Turing machine with binary alphabet and no blank symbol, we may use the following notations:

  •   is the 1-ary symbol for the configuration of the whole tape after   steps (which we may write as a number with LSB first, the value of the m-th location on the tape being its m-th least significant bit). In particular   is the initial configuration of the tape, which corresponds the input to the machine.
  •   is the 1-ary symbol for the Turing machine state after   steps. In particular,  , the initial state of the Turing machine.
  •   is the 1-ary symbol for the Turing machine location on the tape after   steps. In particular  .
  •   is the transition function of the Turing machine, written as a function from a doublet (machine state, bit read by the machine) to a triplet (new machine state, bit written by the machine, +1 or -1 machine movement along the tape).
  •   is the j-th bit of a number  . This can be written as a first-order arithmetic formula with no unbounded quantifiers.

For a prefix-free Turing machine we may use, for input n, the initial tape configuration   where cat stands for concatenation; thus   is a  length string of   followed by   and then by  .

The operation of the Turing machine at the first   steps can thus be written as the conjunction of the initial conditions and the following formulas, quantified over   for all  :

  •  . Since M has a finite domain, this can be replaced by a first-order quantifier-free arithmetic formula. The exact formula obviously depends on M.
  •  
  •  . Note that at the first   steps,   never arrives at a location along the tape greater than  . Thus the universal quantifier over j can be bounded by  +1, as bits beyond this location have no relevance for the machine's operation.

T halts on input   at time   at most if and only if   is satisfied, where:

 

This is a first-order arithmetic formula with no unbounded quantifiers, i.e. it is in  .

Recursively enumerable setsEdit

Let   be a set that can be recursively enumerated by a Turing machine. Then there is a Turing machine   that for every   in  ,   halts when given   as an input.

This can be formalized by the first-order arithmetical formula presented above. The members of   are the numbers   satisfying the following formula:

 

This formula is in  . Therefore,   is in  . Thus every recursively enumerable set is in  .

The converse is true as well: for every formula   in   with k existential quantifiers, we may enumerate the  –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  , and thus enumerates its corresponding set.

Oracle machinesEdit

Similarly, the operation of an oracle machine   with an oracle O that halts after at most   steps on input   can be described by a first-order formula  , except that the formula   now includes:

  • A new predicate,  , giving the oracle answer. This predicate must satisfy some formula to be discussed below.
  • An additional tape - the oracle tape - on which   has to write the number m for every call O(m) to the oracle; writing on this tape can be logically formalized in a similar manner to writing on the machine's tape. Note that an oracle machine that halts after at most   steps has time to write at most   digits on the oracle tape. So the oracle can only be called with numbers m satisfying  .

If the oracle is for a decision problem,   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  . Then   halts on   after at most   steps if and only if the following formula is satisfied:  

where   is a first-order formula with no unbounded quantifiers.

Turing jumpEdit

If O is an oracle to the halting problem of a machine  , then   is the same as "there exists   such that   starting with input m is at the halting state after   steps". Thus:   where   is a first-order formula that formalizes  . If   is a Turing machine (with no oracle),   is in   (i.e. it has no unbounded quantifiers).

Since there is a finite number of numbers m satisfying  , we may choose the same number of steps for all of them: there is a number  , such that   halts after   steps precisely on those inputs   for which it halts at all.

Moving to prenex normal form, we get that the oracle machine halts on input   if and only if the following formula is satisfied:  

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

Note that we may replace both   and   by a single number - their maximum - without changing the truth value of  . Thus we may write:  

For the oracle to the halting problem over Turing machines,   is in   and   is in  . Thus every set that is recursively enumerable by an oracle machine with an oracle for  , is in  .

The converse is true as well: Suppose   is a formula in   with   existential quantifiers followed by   universal quantifiers. Equivalently,   has  > 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  .

We may thus enumerate the  –tuples of natural numbers and run an oracle machine with an oracle for   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  , and thus enumerates its corresponding set.

Higher Turing jumpsEdit

More generally, suppose every set that is recursively enumerable by an oracle machine with an oracle for   is in  . Then for an oracle machine with an oracle for  ,   is in  .

Since   is the same as   for the previous Turing jump, it can be constructed (as we have just done with   above) so that   in  . After moving to prenex formal form the new   is in  .

By induction, every set that is recursively enumerable by an oracle machine with an oracle for  , is in  .

The other direction can be proven by induction as well: Suppose every formula in   can be enumerated by an oracle machine with an oracle for  .

Now Suppose   is a formula in   with   existential quantifiers followed by   universal quantifiers etc. Equivalently,   has  > existential quantifiers followed by a negation of a formula in  ; the latter formula can be enumerated by an oracle machine with an oracle for   and can thus be checked immediately by an oracle for  .

We may thus enumerate the  –tuples of natural numbers and run an oracle machine with an oracle for   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  , and thus enumerates its corresponding set.

ReferencesEdit

Rogers, H. The Theory of Recursive Functions and Effective Computability, MIT Press. ISBN 0-262-68052-1; ISBN 0-07-053522-1

Soare, R. Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1987. ISBN 3-540-15299-7