[FOM] Is current computability theory intuitionistic?
WILLIAM TAIT
williamtait at mac.com
Fri Jun 28 00:23:38 EDT 2013
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
More information about the FOM
mailing list