[FOM] Henk's Characterization of Recursivity

Ali Enayat enayat at american.edu
Thu Jul 1 16:45:41 EDT 2004

The purpose of this note is to outline my explanation of Csaba Henk's
characterization of recursivity in terms of "faithful extensions", posted on
June 1, 2004. Recall that Henk's "faithful" embeddings are known as *end
extensions* in the literature of models of set theory and arithmetic.

In his original posting, Henk asked whether his characterization is new or
not. In my judgment the characterization is new, in the sense that it has
not appeared in print before, but I also believe that it follows from
standard arguments and should therefore be considered folklore.

Both Henk and I would be very interested to hear the opinion of others, of

I initially thought that the characterization follows from preservation
properties of Sigma_1 formulae. In my latest posting (June 6) I first
retracted my claim after Henk pointed out that my suggested proof
establishes a weaker version of his result, and then I put forward the claim
that Henk's result follows from another known line of argument related to
the proof of Trahtenbrot's theorem. Henk's recent posting requested a more
clear explanation. I am responding noe to Henk's request by attempting a
more perspicuous outline of my claim.


Let's begin with the classical characterization of recursivity in terms of
TM's (Turing Machines):

1. A set X is recursive if there is a (deterministic) TM which can "decide"
all questions of the form "is q in X?".  In other words, X is recursive if
there a TM with the following properties:

(a)     T outputs a single symbol iff T reaches a halting state.

(b)     T either outputs s=0 or s=1 if T reaches the halting state.

(c)     For every input q, there exists a natural number t such that T halts
after t steps.

(d)     T outputs 1 on input q iff q is in X.

2. Some definitions:

(a) Let us call a TM with properties (a) and (b) a DECISIVE TM. Note that
(c) and (d) are not included in this definition.

(b) Suppose T is a decisive TM. Let us say "T accepts q" (T rejects q) if T
outputs 1 (T outputs 0), when q is the input of T. Also, let us say "T
decides q" if either T accepts q, or T rejects q.

3. Suppose phi = phi(v_1,...,v_n)  is a formula of set theory whose free
variables are v_1,...,v_n. We say that phi is *bounded* if every quantifier
occurring in phi is bounded, i.e, quantifiers of phi are of the following
forms only:

(a)     For all x, if x is a member of y, then ...
(b)     There exists a member x of y such that ...

(Bounded formulae are also known as Delta_0, Sigma_0, and Pi_0 formulae).

4. Suppose A is end extended by B, where A and B are models appropriate to
the language of set theory, a_1,...,a_n are members of A, and
phi(v_1,...,v_n) is a bounded formula. Then

phi(a_1,...,a_n) is true in A iff phi(a_1,..., a_n) is true in B.

In other words, bounded formulae are absolute for end extensions. This is
verified by a routine induction on the complexity of formulae.

5. Suppose t,e, s, and q are natural numbers. The statement "After t steps,
the e-th decisive TM outputs s, when provided with q as input" can be
expressed as a bounded formula. This is definitely classical, and in my
judgement has been known **at least** since the discovery of Tranhtenbrot's

6. We can now explain the "hard" direction of Henk's characterization:
Suppose X is a recursive set. Then there is some decisive TM T that
witnesses the recursivity of X (as in (1) above).

Consider the formula phi(x) = "the e-th decisive TM accepts x", where T is
the e-th decisive TM.

Let V be the set of hereditarily finite sets. By (1) through (5), for every
q, there is some initial segment F(q) of V such that F(q) satisfies "T
decides q". Therefore the following are equivalent:

(i)     V satisfies phi(q)
(ii)     F(q) satisfies phi(q)
(iii)     Every end extension of F(q) satisfies phi(q).


Ali Enayat
Department of Mathematics and Statistics
American University
4400 Massachusetts Ave, NW
Washington, DC 20016-8050
(202) 885-3168

More information about the FOM mailing list