[FOM] Is current computability theory intuitionistic?
aa at tau.ac.il
Tue Jun 18 21:58:01 EDT 2013
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.
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
More information about the FOM