[FOM] Re: A new characterization of recursivity

[Ali Enayat]

In my earlier posting (in reply to Csaba Henk) I mentioned a result of
Feferman characterizing formulae that are "upward" persistent under end
extensions as those equivalent to Sigma_1 formulae. Upon further reflection,
I realized that one only needs the following special case in order to
establish Henk's elegant characterization:

Proposition. Suppose phi(x) is an arithmetical formula such that the
solution set of phi is not an r.e. set. Then there is a model M of PA, and
some natural number k, such that phi(k) holds (i.e., phi(k) is true in the
standard model N of arithmetic), but phi(k) fails in M.

Proof: The proof is based on the simple but crucial observation that
predicate P(x) defined via "PA proves phi(x)" has an r.e. solution set.
Clearly for all natural numbers n, P(n) implies phi(n). Since the solution
set of phi is not an r.e. set, there must be some natural number k such that
P(k) is false and phi(k) holds. Therefore the theory [PA + not phi(k)] is
consistent and hence has a model M, which is our desired model.

In the context of Henk's characterization, the standard model N is replaced
by  V_omega = hereditarily finite sets, and the model M is replaced by a
nonstandard model of finite set theory *end extending* V. This is all done
via Ackerman's well-known interpretation of set theory within arithmetic via
base 2 coding.