[FOM] Alternative foundations?

[Freek Wiedijk]

Dear Henk,

>Set theory is a very awkward theory to represent
>computations.  It can be done in principle, by describing
>Turing Machines as sets of quadruples,

Surely, a mathematician that used a system based on set
theory wouldn't formalize computability through Turing
machines, but in the style of recursion theory, with the
computable functions being inductively defined as the
smallest set of functions closed under some procedures?
That seems much more attractive than formalizing Turing
machines.

Suppose I _would_ be interested in computability, and
wanted to talk about Turing degrees.  How would the fact
that type theory has a built-in notion of computation help
me with that?  And even in a set theory, I wouldn't need to
define Turing reducibility by talking about Turing machines
if I didn't feel like it, right?

Of course, just as set theories and type theories are
bi-interpretable (see for example Aczel's "On relating
type theories and set theories" from 1998), a definition
of computable functions in terms of Turing machines is
equivalent to a definition in a more mathematical style.
So from a mathematician's point of view, who cares which
definition is taken to be the primitive one?

And notice that type theory doesn't give you _all_ computable
functions, as it only allows one to define _total_ computable
functions.  And of course that means not even _all_ total
computable functions.

Also note that Steven Obua added a computational model (a
"Poincaré principle") to Isabelle, in his PhD thesis.

Both in the case of type theory and in Obua's work,
one might consider the foundations to be "cheating",
because one hardwires in some notion of computation (for
philosophical reasons, or for efficiency) that could just
as well be described _without_ it being hardwired in.

Finally, I think the Flyspeck project is _not_ relying on
the computational model that is hardwired into type theory,
because those people use a HOL-based system?  Admittedly,
it's causing them problems (because they cannot "cheat"), but
still they don't seem to be switching to Coq for this reason?

Freek