FOM: HA and Post's Problem

Stephen G Simpson simpson at
Fri Sep 22 19:21:45 EDT 2000

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 ]
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

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

More information about the FOM mailing list