FOM: HA does not solve Post's Problem; foundational significance

[Stephen G Simpson]

Post's Problem (1944) is the problem of finding an r.e. Turing degree
which is intermediate, i.e., neither recursive nor Turing complete.

Post's Problem was classically solved by Friedberg and Muchnik
(1956/1957), who constructed a pair of incomparable r.e. degrees.
Their incomparability proof used an apparently highly nonconstructive
method, the Priority Method, which has played a dominant role in
subsequent extensive recursion-theoretic investigation of
r.e. degrees, r.e. sets, etc.

In my FOM posting of 7 Aug 2000, I conjectured that HA (Heyting
Arithmetic, a.k.a. intuitionistic first order number theory) is
consistent with every nonrecursive r.e. set being many-one complete,
hence Turing complete.  I also sketched a proof of my conjecture.  I
thank Andrej Bauer for an offline comment on the sketch.

It turns out that my August 7 sketch is correct.  However, here is a
more direct proof, using an idea of Myhill (1955) as expounded by
Odifreddi, Classical Recursion Theory, 1989, page 305.

We use recursive realizability in the sense of Kleene, Introduction to
Metamathematics, 1950, pages 501-516.  It is enough to find a
realization of the statement "every nonrecursive r.e. set is many-one
complete".  We do this as follows.  Suppose we are given (an index of)
an r.e. set A, together with a realization of "A is nonrecursive".  In
particular, we have (an index of) a total recursive function f such
that for all e, f(e) witnesses that the partial recursive function {e}
with index e differs from the characteristic function c_A of A.  In
other words, for all e, f(e)=n where {e}(n) is undefined or unequal to
c_A(n).  Now suppose we are also given (an index of) an arbitrary
r.e. set B.  By the S-m-n Theorem, we can effectively find (an index
of) a primitive recursive function g such that, for all x and all n,
{g(x)}(n)=0 if x gets enumerated into B before n gets enumerated into
A, {g(x)}(n)=1 if n gets enumerated into A before x gets enumerated
into B, and {g(x)}(n) is undefined otherwise.  For all x we have that
{g(x)}(f(g(x))) is undefined or unequal to c_A(f(g(x)).  It follows
that, for all x, x belongs to B if and only if f(g(x)) belongs to A.
Thus we have effectively found a realization of "A is many-one
complete".  This proves the conjecture.

The foundational significance of this result is that the
Friedberg/Muchnik solution of Post's Problem is inherently
nonconstructive.  This lends weight to the idea that the Priority
Method itself may be inherently nonconstructive.  Such a conclusion
would be of interest with respect to our earlier FOM discussion of
priority arguments and recursive counterexamples (FOM, July 2000).  In
order to obtain constructive information, it seems desirable to
eliminate priority arguments whenever possible.

-- Steve