[FOM] Is current computability theory intuitionistic?

[Dustin Wehr]

Agreed, and there are distinct notions of "constructive" for each
sufficiently-robust complexity class. I sometimes think that
complexity theorists are more seriously interested in constructive
proofs than most intuitionists, in the sense that they usually aren't
completely satisfied with a proof until its constructive component has
been made as efficient as is thought possible (well, often polynomial
time is taken as satisfactory, but in some contexts, such as bounded
arithmetic, there is motivation to be more refined than that). The
celebrated probabilistic-polynomial-time-constructive proof of the
Lovasz Local Lemma is a somewhat recent example.

And despite that, I've never seen intuitionistic logic used explicitly
in complexity theory.

Dustin

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