[FOM] Is current computability theory intuitionistic?
hancock at spamcop.net
Wed Jun 26 18:05:40 EDT 2013
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
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 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?
More information about the FOM