[FOM] Proof. was: Checkers is a draw
Timothy Y. Chow
tchow at alum.mit.edu
Sun Jul 29 19:44:14 EDT 2007
On Sun, 29 Jul 2007, Bill Taylor wrote:
> IMHO this distinction between computation and deduction is rather
> 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.
More information about the FOM