[FOM] Is current computability theory intuitionistic?

[Peter Hancock]

Hi Bill,

I'm pretty sure you can answer these questions quickly.

> where in the `hierarchy of formal
> systems' S does the equivalence
>
> \forall x \exists y T(e,x, y) is provable in classical S iff it is
> provable in intuitionistic S
>
> break down. As long as the double negation interpretation of S
> classical in S intuitionistic is valid the equivalence holds.

If understand it, the double-negation translation breaks down for ID_i for
i > 0 (for example the theory of the Church-Kleene second number class).
Is it nevertheless true that the classical and intuitionistic versions
prove the same Turing machines are total?  I simply don't know.  Did
Buchholz, Pohlers or someone prove something like this?

>Does it hold
> for ZF (where intuitionistic ZF is some version of constructive set
> theory)?

I though Harvey Friedman showed that ZF was DN-interpretable in IZF, for some
slightly bureaucratic value of IZF?

Just one more question:

> So it holds for number theory of finite order for example.

Where "it" is the double negation interpretation.  So that's PA^w vs. HA^w,
I'm guessing.

I thought HA^w was no stronger than HA, whereas PA^w was (is?) as strong as Church's
simple type theory over the type of natural numbers, ie. grotesquely stronger than
PA.  What's my mistake?

Highest regards,

Peter