[FOM] Is current computability theory intuitionistic?

[WILLIAM TAIT]

Craig,

If my question is 'ill-posed' because "constructive" is a vague concept, then it is doubly ill-posed, since so is "classical" ("nonconstructive").

The lack of precision of the concept "constructive" does not in itself make the question unanswerable. For example---although I agree that this question is significantly different from mine---I think we would agree on the answer to the question of whether the intermediate value theorem is constructively valid. 

I note that, besides Peter Hancock's note, my question has not set the FOM world on fire; so maybe we can take the discussion offline---or better, you can hike a few miles over and we can have lunch.

Bill 

On Jun 26, 2013, at 5:23 PM, Craig Smorynski <smorynski at sbcglobal.net> wrote:

> The problem is that "constructive" is a vague concept. If you make it precise by saying constructivity means provable in this formal system, one can attack the problem. I am inclined to think that talk of "constructivity" and ZF makes no sense. Certainly one can do a formally intuitionistic version of ZF, but as to an actually constructive theory of the sort is hard for me to swallow. So I would imagine that a truly constructive theory would fall well short of ZF. If there is a last one that is primitive recursively axiomatisable, ZF ought to be able to prove its sigma_1 soundness and thus offer an enumeration of its provably recursive functions.
> 
> Without such a theory I would consider the question ill-posed.
> 
> On Jun 26, 2013, at 2:17 PM, WILLIAM TAIT wrote:
> 
>> 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'}.
>> 
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
> 
> Craig
> 
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom