[FOM] Re: Henk's Characerization of Recusivity

[Henk Csaba]

On Wed, Jul 14, 2004 at 12:08:33PM -0400, Ali Enayat wrote:
> 
> This is a response to Henk's comments (July 10) on my most recent attempt
> at explaining his charcterization of recursivity. in my July 1 posting.
> 
> I believe that Henk and I are very close to "converging". Indeed the whole
> issue at this point hinges on whether Henk can convincingly defend the
> following claim of his, when he writes:
> 
> >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.
> 
> Here F(q) is a sufficiently large finite portion of the hereditarily finite
> sets, in which one can recognize a specific Turing machine (in this case
> the e-th "DECISIVE TM") to have reached a halting state and produced either
> a 0 or a 1. This latter statement is a bounded statement, and will remain
> true in any end extension of F(q), no matter how pathological. To put it
> dramatically: A dead Turing machine cannot be resurrected, even in a
> nonstandard universe.

A bounded statement will mean what it should mean in all end extensions,
even in the most pathological ones, for sure. The problem is: exactly which
of our players qualify as a bounded statement?

Of course, we can agree in some standardized representation of TM runs in
the first-order language of finite set theory. Now
the following will be bounded:

"c is a finished computation of the e-th decisive TM on input x, and the
halting state of c is 0";

"c is a finished computation of the e-th decisive TM on input x, and the
halting state of c is 1";

"c is a finished computation of the e-th decisive TM on input x, and the
halting state of c is either 0 or 1".

In the above statements e is to be treated as a parameter (the algorithm/TM
is fixed during the current discourse, thus so is its index), hence if we
formalized them, they would turn to formulas with *two* free variables, c and
x.

So far so good. But now let's turn to our mission. We start with having some
property of hereditarily finite sets P(x) which is decidable. We seek a such
a formalization of P(x) which fulfills the criteria set by me in my
thread-starter post. Syntactically this formalization should be a
first-order formula with one free variable. Now following your train of
tought, let's utilize TM's: since we know that P(x) is decidable, there is some
decisive TM which spits out 1 on x if P(x), and spits out 0 on x if not
P(x); let the index of this TM be e.

Now, if we try to formalize P(x) via the e-th decisive TM, the following
statements seem to be possibly usable:

"the e-th decisive TM halts on x with 0";
"the e-th decisive TM halts on x with 1";
"the e-th decisive TM halts on x with either 0 or 1"

(the second is equivalent with P(x)).

The difference is that these latter statements speak only of x, so a
formalization of them should be a formula with only *one* free variable, x.
They don't include reference to the computation c.

The typical formalizations of these latter statements is gained by applying a
"there exists c" quantification on the respective formalizations of the
first kind of statements. (This is what I tried to demonstrate in my
previous post.) There is no general constructive way for producing c, you
can just say "there exists c" (or tell me if you see one). And we get out
of the realm of bounded formulas by this step. So there is no safety wrt.
end extensions anymore. Not this way, at least.

* * *

I do an attempt of summarizing of those issues which lead easily to errors.

We have the P(x) property. Given any particular x_0, we have the proposition
"x_0 has the P proprety". This can be formalized as a bounded formula with
no free variable: prior to formalization, we put together the description of
the run of the e-th decisive TM on x_0, it can be turned to a bounded
definition of some object c_0, and we can substitute this to the bounded
formula coming from

"c is a finished computation of the e-th decisive TM on input x, and the
halting state of c is 1",

(in place of c), moreover we can subsitute x_0 to this formula in place of x,
and thus we really got a bounded formula with no free variable, being 
equivalent with "x_0 has the P proprety". Up to this point we agree, I
think.

*The problem is that it is not what we need.*

We need *one piece of* first-order formula theta(x) with one free variable
such that given any particular x_0, performing a pure syntactical
substitution of x_0 to theta(x), the yielded formula theta_{x_0} has the
following property:

"""
there is a finite sub-universe F such that the truth value of theta_{x_0}
on F and the truth value of theta_{x_0} on an arbitrary end extension of F
is the same.
"""

If you re-read my initial post you will see that this is what we need. But
in this case you can't use practices specific to x_0 in order to produce the
respective computation object. 
 
> If I am wrong, and such a counterexample can be convincingly exhibited,
> then I for one would gladly welocome Henk's characterization as a new one.

Suggest strategies of formalizing the one-variable statement 

"the e-th decisive TM halts on x with 1"

(not strategies of formalizing the proposition "the e-th decisive TM halts
on x_0 with 1", where some particular x_0 is chosen).

Then I will have the possibility of saying you "well, you are right, this
kind of formalization does the job", or showing a counterexample why it is
not so.

I can't show counterexamples to your statements, as they are true. You just
seem to miss the point: these statements verify something else, not my
claim.

Yours,
-- 
Csaba Henk

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