[FOM] Is current computability theory intuitionistic?

[WILLIAM TAIT]

Craig,

The first part of your response does miss something, namely the "(by whatever means)".

Yes,  \forall x \exists y T(e,x, y) is provable in PA iff it is provable in HA. But that wasn't my question. It does raise the further question however  of 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. So it holds for number theory of finite order for example.  Does it hold for ZF (where intuitionistic ZF is some version of constructive set theory)?  


The second part of your response  may also miss something: can you give me an example of a function provably computable in ZF that is not provably computable by constructive means?  Note that I am NOT asking whether there is a Turing machine e such that {e} is provably total in e.g. ZF but not provably total constructively. Im asking for an e such that {e} is provably total non-constructively and no {f} with {e} = {f} is provably total constructively.  

Sorry if I caused confusion.

Bill
 
On Jun 25, 2013, at 2:59 PM, Craig Smorynski <smorynski at sbcglobal.net> wrote:

> Am I missing something? PA and HA have the same provably computable functions, so the two theories would have to have different strengths. Otherwise the answer is yes even for both theories classical, provided one has more provably computable functions, e.g. ZF vs. PA.
> 
> Or am I missing something?
> 
> On Jun 19, 2013, at 4:36 PM, WILLIAM TAIT wrote:
> 
>> Maybe an interesting question in this connection is whether there is an e such that
>> 
>> \forall x \exists y T(e,x, y)
>> 
>> is classically provable (by whatever means) but there is no e' such that 
>> 
>> \forall x \exists y T(e',x, y)
>> 
>> is constructively provable and {e} = {e'}.