[FOM] Is current computability theory intuitionistic?

[WILLIAM TAIT]

On Jun 26, 2013, at 5:05 PM, Peter Hancock <hancock at spamcop.net> wrote:

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

It seems so. Cut-elimination for classical ID_i is provable for arithmetic sentences in (some low fragment of) intuitionistic ID_{i+1}. (My Buffalo conference paper from1968.) But I don't know how constructivists in general feel about ID_i for i > 1 (e.g. about the higher constructive number classes). Maybe there is no 'in general'. 

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

He shows that a system S obtained from ZF by omitting extensionality and weakening powerset is DN interpretable in intuitionistic ZF- extensionality (i.e. ZF without extensionality and using only intuitionistic logic). He then shows that ZF is interpretable in S. I keep confusing myself, but I think this refutes Craig's suggestion that ZF can enumerate the intuitionistic ZF computable functions---at least for this version of constructive ZF. 

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

The notation PA^w and HA^w is ambiguous: it can mean quantification over functions of higher finite order or over sets of higher finite order. In the classical case, it makes no difference, since very set has a characteristic function. But of course this fails in the intuitionistic system. In the first case, HA^w is interpretable in HA, coding the functions (as effective operations) by their Turing machines. In the second case PA^w is DN interpretable in HA^w.

Very best regards,
Bill