[FOM] Re: A new characterization of recursivity

[Henk@degas.ceu.hu]

On Wed, Jun 02, 2004 at 12:18:43PM -0400, Ali Enayat wrote:
 
> It is easy to see that if A is end extended by B, then Sigma_1 predicates
> are upward absolute (and conversely, Pi_1 predicates are downward absloute).
> Here the classification Sigma_n / Pi_n is as in arithmetic and set theory,
> where bounded quantification does not increase the complexity. 

Hm, I can't follow this reasoning in all details.

Tersely: I don't see how can you put together the preservation-style
characterizations of Sigma_1 and Pi_1 and gain a preservation-style
characterization of Delta_1 from it.

In a bit more verbose manner:

What I see (V is standard model of finite set theory):

If a subset X of V is Sigma_1, then by upward absoluteness of Sigma_1
predicates we have:

there is a Sigma_1 formula f(x) such that

i) f(x) defines X in V;
ii) for any q in X, there is a finite subset F of V such that
  * F includes q;
  * for any faithful embedding (aka. P-extension, end extension) i: F -> B
    B |= f(i(q)).

Similarly:

If a subset X of V is Pi_1, then by downward absoluteness of Pi_1 predicates
we have:

there is a Pi_1 formula g(x) such that

i) g(x) defines X in V;
ii) for any q not in X, there is a finite subset F of V such that
  * F includes q;
  * for any faithful embedding i: F -> B
    B !|= g(i(q)) ["!" means not here].

>From this, by "recursive <=> Sigma_1 and Pi_1" we get: 

If a subset X of V is recursive, then there is Sigma_1 formula f(x) and a
Pi_1 formula g(x) such that

i) both of f(x), g(x) define X in V;
ii) for any q in X, there is a finite subset F of V such that
  * F includes q;
  * for any faithful embedding i: F -> B
    B |= f(i(q));
iii) for any q not in X, there is a finite subset F of V such that
  * F includes q;
  * for any faithful embedding i: F -> B
    B !|= g(i(q))          

-- this characterization is weaker than the one I gave, and I see no easy
way to deduce my one from this. If you see, I'd appreciate if you told me
how.

> The converse
> also happens to be true and is due to Feferman, and immediately yields
> Henk's characterization (modulo well-known arguments). I am curious,
> however, whether Henk's proof involves different ideas or not.
> 
> Feferman's result appears in:
> 
> Feferman, Solomon
> Persistent and invariant formulas for outer extensions.
> Compositio Math. 20 1968 29--52 (1968).
> 
> It is worth pointing out that Feferman used a proof theoretic argument to
> establish his result. Later Marker found a model theoretic argument (using
> recursively saturated models):
> 
> Marker, David
> A model theoretic proof of Feferman's preservation theorem.
> Notre Dame J. Formal Logic 25 (1984), no. 3, 213--216.
 
I think this is the easier direction. Thank you for the references, they are
very apt to the problem, and I didn't know them. However, one can easily
prove this direction directly, eg., as you did in your other reply.

-- 
Csaba Henk

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