[FOM] Is current computability theory intuitionistic?
WILLIAM TAIT
williamtait at mac.com
Wed Jun 19 17:36:56 EDT 2013
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
More information about the FOM
mailing list