[FOM] Re: A new characterization of recursivity

[Ali Enayat]

This is a reply to Csaba Henk's recent query (Tuesday, June 1, reproduced
below) concerning a "set theoretic" characterization of recursivity.

Faithful embeddings (as defined in Henk's note) also called "end embeddings"
in the literature (note that a model A is faithfully embedded in a model B
via an embedding i, if B is an end extension of i(A)).

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. 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.


Regards,

Ali Enayat


**************************************

>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.)