[FOM] Is current computability theory intuitionistic?

[Vasco Brattka]

Dear Steve

Only very elementary parts of computability theory are computable.

As soon as you get to more interesting "constructions", then the
corresponding results turn out to be non-computable and hence
non-constructive (i.e. not intuitionistically provable).

For instance, the Low Basis Theorem states that every infinite
computable binary tree has a low path. But there cannot be any
algorithm that given a tree finds such a path in general (due to
the existence of Kleene trees without computable paths) and hence
there cannot be a constructive proof that shows the existence of
such a path.

However, sometimes it also matters how you exactly represent the
objects of interest and even many non-constructive proofs have some
computational content that can be expressed by choosing the right
representation.

For instance, the Low Basis Theorem is uniformly computable, if
you do not want a path as a result, but a sequence that converges
to the Turing jump of a path (i.e. a witness of lowness).

Best regards

Vasco Brattka






> Today's Topics:
>
>     1. Is current computability theory intuitionistic? (Steve Stevenson)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 18 Jun 2013 11:59:49 -0400
> From: Steve Stevenson <steve at clemson.edu>
> To: Foundations of FOM <fom at cs.nyu.edu>
> Subject: [FOM] Is current computability theory intuitionistic?
> Message-ID:
> 	<CAKoJ0==rY6DZ1Umh7qNa+B2amoBFHYO9gPChgmGMYObVeCw+fw at mail.gmail.com>
> Content-Type: text/plain; charset=ISO-8859-1
>
> I didn't know to ask this question when I was learning and now I'm too
> old to read all the standard books. My recollection though is that
> computability texts use classical logic. Is that true? Does it matter?
>
> --
> D. E. (Steve) Stevenson, PhD, Emeritus Associate Professor, Clemson University
> "Those that know, do. Those that understand, teach," Aristotle.
>
>
> ------------------------------