[FOM] Is current computability theory intuitionistic?

[Carl Mummert]

On Tue, Jun 18, 2013 at 11:59 AM, Steve Stevenson <steve at clemson.edu> wrote:

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

It is certainly true. As with any other mathematical subject that is not
intentionally studied constructively, classical logic is used throughout
recursion theory. For example,

* It would be routine in computability theory to assert that a given Turing
machine, on a given input, which is proven to not run forever, must halt
after some fixed number of steps. This form of Markov's principle is not
universally accepted among constructivists.

* The classical equivalence between sets and their characteristic functions
is taken for granted. This equivalence is not valid constructively, because
a set of natural numbers with a characteristic function must be decidable
in the constructive sense (each number either is, or is not, a member of a
given set), while several popular constructive systems do not prove that
every set of natural numbers is decidable in the constructive sense.

There are many more examples, but these highlight how early in the subject
the constructive and classical theories will begin to diverge. Perhaps more
importantly, the way in which the subjects diverge depends on the
particular constructive theory being used (for example, HA^\omega and CZF
differ in key respects).

I would suspect that someone must have studied constructive recursion
theory, to see how much of the classical theory goes through, but I don't
know of a good reference. There is certainly much more research on
constructive type theory.

I do not believe that the question whether the use of classical logic
matters in recursion theory can be separated from the same question about
mathematics in general. The usual arguments about classical and
constructive mathematics will apply.

- Carl

-- 
Carl Mummert
Assistant Professor of Mathematics
Marshall University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130619/fbc1f3cc/attachment.html>