[FOM] Is current computability theory intuitionistic?
Vasco Brattka
Vasco.Brattka at cca-net.de
Wed Jun 19 16:47:11 EDT 2013
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.
>
>
> ------------------------------
More information about the FOM
mailing list