[FOM] Henk's Characterization of Recursivity

[Csaba Henk]

On Thu, Jul 01, 2004 at 04:45:41PM -0400, Ali Enayat wrote:
> Let's begin with the classical characterization of recursivity in terms of
> TM's (Turing Machines):
> 
> 1. A set X is recursive if there is a (deterministic) TM which can "decide"
> all questions of the form "is q in X?".  In other words, X is recursive if
> there a TM with the following properties:
> 
> (a)     T outputs a single symbol iff T reaches a halting state.
> 
> (b)     T either outputs s=0 or s=1 if T reaches the halting state.
> 
> (c)     For every input q, there exists a natural number t such that T halts
> after t steps.
> 
> (d)     T outputs 1 on input q iff q is in X.
> 
> 2. Some definitions:
> 
> (a) Let us call a TM with properties (a) and (b) a DECISIVE TM. Note that
> (c) and (d) are not included in this definition.
> 
> (b) Suppose T is a decisive TM. Let us say "T accepts q" (T rejects q) if T
> outputs 1 (T outputs 0), when q is the input of T. Also, let us say "T
> decides q" if either T accepts q, or T rejects q.

[snip]

> 
> 5. Suppose t,e, s, and q are natural numbers. The statement "After t steps,
> the e-th decisive TM outputs s, when provided with q as input" can be
> expressed as a bounded formula. This is definitely classical, and in my
> judgement has been known **at least** since the discovery of Tranhtenbrot's
> theorem.

For making back-reference easy, let's call your bounded formula
psi(t,e,s,q), or if the TM (so its index e) is fixed, psi_e(t,s,q).  

> 6. We can now explain the "hard" direction of Henk's characterization:
> Suppose X is a recursive set. Then there is some decisive TM T that
> witnesses the recursivity of X (as in (1) above).
> 
> Consider the formula phi(x) = "the e-th decisive TM accepts x", where T is
> the e-th decisive TM.

What is phi? What I can imagine is that you think of 

"there exists t such that psi_e(t,1,x)",

it's a sigma_1 formula.
 
> Let V be the set of hereditarily finite sets. By (1) through (5), for every
> q, there is some initial segment F(q) of V such that F(q) satisfies "T
> decides q". Therefore the following are equivalent:

This "T decides q" is a bit ambiguous. If we are in V, it's just
equivalent with "True", so then the requirement wrt. F(q) is void.

However, I suppose you'd formalize "T decides q" as follows:

"there exists t such that psi_e(t,0,x) or psi_e(t,1,x)".

> (i)     V satisfies phi(q)
> (ii)     F(q) satisfies phi(q)
> (iii)     Every end extension of F(q) satisfies phi(q).

Now I think you've made mistake here (given that you'd formalize phi in
the way suggested above): (ii) and (iii) are *not*
equivalent. That is, consider the case when q is not in X, ie., T
halts with 0 on q, ie., 

"there exists t such that psi_e(t,0,x)".

In this case, F(q) won't satisfy phi(q), of course.

But it's quite possible that you can end extend F(q) such that phi(q)
will be valid in the extension -- so, in this pathological extension

"there exists t, t' such that psi_e(t,0,x) and psi_e(t',1,x)"

will hold.

The difficulty lies in re-formulating the above phi in a safe way, which
can cope with those "pathological" extensions. It is possible -- it's
neither trivial nor too hard, doing this doesn't require a genius, one
just have to build the formula carefully, the whole procedure resembles
the way how Rosser extended the scope of Godel's noncompleteness result from  
omega-consistent Peano models to arbitrary ones.

Anyway, in my honest opinion the necessity of this re-formulation is
enough for raising my statement above the "folklore" status. 

* * *

One more comment: I re-read your proof for the "easy" direction, thanks
for that, it's really an elegant solution, much sorter than my original
one.

Regards,
-- 
Csaba Henk

"There's more to life, than books, you know but not much more..."
[The Smiths]