[FOM] Do you know of the equivalence of recursivity and the following... ?

[tphhec01@degas.ceu.hu]

Dear FOM-ers,

I cooked up the following rewording of recursivity, and I'd like to know
whether it is now a genuine result, or it is a well-known fact. In the
latter case, please be as kind as to give references. 

Nb. the following stuff is presented in the scope of finite set theory, but
it would be easy to "port" the statement to arithmetic (a bit more common
playground), it's just then it would become slightly more technical.

		* * *

"E" will denote the set-theoretic membership relation.
"V" will denote the standard model of finite set theory (the set of
hereditarily finite sets).

Def.: Let A, B be E-type structures (ie., their similarity type consists of
the binary rel. symbol "E"), and i: A -> B be an embedding. We say that i is
_faithful_, if for any a in A and b in B such that b E i(a) [here E is E of
B], there is an a' in A such that b = i(a'); that is, the i-image of A is a
downward closed subset of B wrt. the transitive closure of E.

Thm.: A subset X of V is recursive iff there is a first-order formula f(x)
such that

i) f(x) defines X in V;
ii) for any q in V, there is a finite subset F of V such that
  * F includes q;
  * for any faithful embedding i: F -> B (here B is an *arbitrary* E-type 
    structure, no set-theoretic axiom is required!) 
   
                                 V |= f(q) <=> B |= f(i(q)) .

(Intuitively, a set is recursive iff for any object there is a finite
witness showing that object belongs / doesn't belong to the set; this might
be used in some "pro Church Thesis" argument.)

 
Thanks,
__
Csaba Henk

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