[FOM] Is current computability theory intuitionistic?

Peter Hancock hancock at spamcop.net
Wed Jun 26 18:05:40 EDT 2013

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,


More information about the FOM mailing list