[FOM] Proof. was: Checkers is a draw

[Timothy Y. Chow]

On Sun, 29 Jul 2007, Bill Taylor wrote:
> IMHO this distinction between computation and deduction is rather 
> artificial,
[...]
> The ontology of proof has been (for most) fully decided and 
> crystal-clear since about 1906 or so.

Spoken like a pure mathematician!

The issue under discussion was not a philosophical one, but a practical 
one.  A "mere" exponential blowup does not, in my opinion or yours, make
any qualitative philosophical difference.  But it does make a practical 
difference.  A formal proof of length N that is wrong with probability 
1/2^n is quite different from a formal proof of length 2^N that is wrong 
with probability 1/2.

Due to lack of education, I was unaware of some of the subtleties 
mentioned by Krishnaswami.  I hope to remedy that by getting my hands 
dirty with HOL Light, which I just downloaded.

Tim