
Just now I began thinking about Marvin Minsky's proof that
Fermat's last theorem is decidable. 
It has of course been recently decided affirmative.

His proof ran as follows. Reconsider the process of trying all
integers looking for a solution. Either this process halts
and the theorem is false, or it doesn't, and the theorem is true.
If the theorem was undecidable, then the process couldn't halt,
so it must run forever hence the theorem is true. So it is decidable,
contradicting the hypotheses.

This seemed OK, but it bothered me since one could say the
same for halting of a machine. Indeed, given a specific machine M,
this argument would say that the halting of M was decidable.
This should not be confused with the halting problem for a "general"
machine X. But what does it mean, a "general" machine?

The algorithm for the halting of machine M is one of:
   1) Answer Yes
   2) Answer No
And we can assume an oracle choses (correctly!) option 1 or 2 for us.
There is no contradiction here.

For a "general" machine, was must assume a function N -> {Yes, No}.
The existence of this function can be assured, again by oracle.
However the pattern of Yes's and No's of this function are not
computable. In front of this function, our computers, indeed ourselves,
are as a very young child confronted with a problem in elementary
arithmetic. We know that there is an answer, but we cannot go about
constructing it. The child's ignorance can be remedied, though he or
she might not be aware of this. "Noncomputability" is a proof that
the similar ignorance for the construction of the halting function is
intrinsic, irremedial and permanant, at least if one is to continue
to abide by the current language of proof and computation.

