[FOM] Is current computability theory intuitionistic?

Fri Jun 28 17:54:09 EDT 2013

It seems to me that all concepts of mathematics are initially vague. People use them as if they know what they were talking about for ages until eventually precise definitions for them emerge. The definitions may or may not agree and, usually one finally emerges supreme. This is not always the case. There are still a lot of competing notions of smoothness: continuity, differentiability, continuous differentiability and a whole hierarchy of C^n functions. Still, one might say something like "let C be a smooth curve". The question of whether or not a smooth curve has a tangent everywhere is unanswerable until you specify which notion of smoothness is meant. The answer is "no" for continuity, but "yes" for differentiability and beyond. Does a smooth curve have an arc-length?

I think "classical" is more precisely pinned down than "constructive". There is a hierarchy of constructivities depending on how liberal one wants to allow one's "constructions" to be. At the bottom we  might find the elementary functions and propositional reasoning, then Hilbert's finitism, all the way up to Bishop's infinitary use of sets in defining the Lebesgue integral. One can meaningfully ask the question for formal theories of each of these theories paired with its classical counterpart or ZFC, but I wouldn't know where to begin with "constructive mathematics" vs "classical mathematics".

Yes, we should get together. I've not been in touch with anyone lately because I've been busy banging my head against the wall trying to understand how the Internet is so full of reports that Bhaskaracharya had anything like the Mean Value Theorem. It does not seem to be anywhere in the Siddhanta Siromani, but my inability to find it may be due in part to all the technical terms given only in Sanskrit in English translations.

On Jun 27, 2013, at 10:26 PM, WILLIAM TAIT wrote:

> 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
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

Craig

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130628/1c573a9f/attachment.html>