FOM: constructivity; priority arguments

[Stephen G Simpson]

In my FOM posting of 28 Jul 2000, I asked:

 > Can we show that some standard results that are standardly proved
 > with priority arguments are not provable constructively?  For
 > example, can we show that the Friedberg/Muchnik Theorem is not
 > provable in HA?

Having thought about the matter some more, I now believe that this is
the case.  I conjecture that HA (Heyting Arithmetic) is consistent
with the statement that every nonrecursive r.e. set is many-one
complete, hence Turing complete.  Perhaps someone more competent than
I with respect to intuitionism will help me finish the proof of this
conjecture.

My idea is that the statement "every nonrecursive r.e. set is many-one
complete" ought to be recursively realizable, as follows.  I use
standard recursion-theoretic notation.  Suppose we are given a
nonrecursive r.e. set A.  Let f be a recursive function which realizes
the nonrecursiveness of A, in the sense that for all e, f(e) is a
witness to the fact that the e-th partial recursive function, {e}, is
not the characteristic function, c_A, of A.  In other words, for all
e, f(e) = n where {e}(n) is not equal to c_A(n).  By the S-m-n
Theorem, let h(x) be a primitive recursive function such that, for all
x with W_x disjoint from A, and for all n, if n belongs to W_x then
{h(x)}(n) = 0, and if n belongs to A then {h(x)}(n) = 1.  Thus, for
all x with W_x disjoint from A, {h(x)} is just c_A restricted to the
union of W_x and A.  It follows that, for all x with W_x disjoint from
A, f(h(x)) does not belong to the union of W_x and A.  This implies
that the r.e. set A is creative in the sense of Post.  It follows by a
result of Myhill that A is many-one complete.  All these arguments
seem to work in HA.

Can someone help me make sense of this idea?

-- Steve