[FOM] Is current computability theory intuitionistic?

[Arnon Avron]

As far as I can judge, the central issue in computability
theory, Church Thesis (or Church-Turing Thesis),
is meaningless from an intuitionistic point of view.

The usual understanding of Church thesis as it is described
and explained in books is certainly classical. It is
assumed that being computable is a property of functions from
N to N (say) such that every function from N to N is either
computable or not, and what the thesis does is to 
characterize those which are. This view of the thesis,
which relies on LEM, is of course not intuitionistic.
Moreover, it is difficult for me to see how can this
thesis possibly be described in any alternative way 
which would make sense from an intuitionistic  point 
of view. Intuitionistically, every function is computable
by the very meaning of the intuitionistic notion of a function.
So Church thesis should intuitionistically say that every
function from N to N is definable by some Turing machine (say).
This claim, in turn,  is intuitionitically acceptable iff
a procedure is given that constructs for every 
function (in the intuitionistic sense) from N to N a corresponding 
Turing machine.  For the best of my knowledge, nobody has provided
such a procedure, or even has given some reason to believe
that such a procedure might be found. 

Arnon Avron


On Tue, Jun 18, 2013 at 11:59:49AM -0400, Steve Stevenson 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?
> 
> --
> D. E. (Steve) Stevenson, PhD, Emeritus Associate Professor, Clemson University
> "Those that know, do. Those that understand, teach," Aristotle.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom