FOM: HA and Post's Problem

[Stephen G Simpson]

Response to Jaap van Oosten, FOM, 20 Sep 2000.

Van Oosten writes:

 > Suppose that one defines "X is Turing reducible to Y" as: There is
 > e, such that for all x there is a y and an s such that s is a
 > Y-information sequence and T(s,e,x,y), and x\in X <==> U(y)=0
 > (where U(y) is the output of computation y) 
 ...

 > HA does not prove "K is Turing reducible to K" for this definition.

OK, I see now.  In fact, HA+CT proves "K is not Turing reducible to
K", right?  But of course HA proves "K is many-one reducible to K"
(trivially, via the identity function).  So HA+CT proves that many-one
reducibility does not imply Turing reducibility, even for r.e. sets,
etc etc.  In short, basic properties of Turing reducibility are lost
in HA+CT, if we define Turing reducibility as above.

I have some experience with formalization of mathematics in
(classical) subsystems of second order arithmetic.  [ The web page for
my book on this subject is http://www.math.psu.edu/simpson/sosoa/. ]
In that context, it is customary to choose definitions in such a way
as to preserve at least the most basic properties of the notions in
question.  I assume there is a similar custom in the intuitionistic
context.

Thus, I am tempted to conclude that the above definition of Turing
reducibility is unsuitable for the intuitionistic context.

Is there no way to modify the definition, to make it more appropriate
for the intuitionistic context?  For example, truth-table reducibility
seems to make perfect sense intuitionistically, just like many-one
reducibility ....

-- Steve