[FOM] Is current computability theory intuitionistic?

[WILLIAM TAIT]

Maybe an interesting question in this connection is whether there is an e such that

\forall x \exists y T(e,x, y)

is classically provable (by whatever means) but there is no e' such that 

\forall x \exists y T(e',x, y)

is constructively provable and {e} = {e'}.

Bill Tait


On Jun 18, 2013, at 4:41 PM, Alasdair Urquhart <urquhart at cs.toronto.edu> wrote:

> Current texts certainly do present computability in terms of classical
> logic.  I recall some example in Hartley Rogers along the lines
> of a function defined by: f(n) = 1 if the Riemann hypothesis is true,
> otherwise 0 (I don't have the book at hand right now).  Rogers
> says that f is a well defined function.
> 
> Whether this matters or not, I am not sure.  I think a lot of computability theory can be easily reworked in a constructive context, since the arguments are generally constructive.  On the other hand,
> the classical arithmetical hierarchy presupposes a classical
> reading of the quantifiers.
> 
> On Tue, 18 Jun 2013, 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