On Fri, 3 Mar 2006, Eugene Salamin wrote:
Such a computer program would be as intricate as the proofs it is expected to verify, and is subject to the same human error. There cannot be certainty of correctness of a proof without certainty of the correctness of the proof-checking software. Could the program check itself?
The proof checker would be a program and not a proof, so the proof checker would not be designed to check the correctness of the program. It seems that the best one could do is to construct a proof that the proof checker works and ask the proof checker to check that. Of course, like any human enterprise there is the possibility of error. Can we perform any task with a guarantee that there will be no error? As long ago as the 1970s I recall hearing of a specialty in computer science called automatic proof verification. Googling around I find many references. For example there is Edmund Clarke at Carnegie Mellon who describes his research interest as: Automatic verification of computer hardware and software: http://www.cs.cmu.edu/~emc/15-398/ Also Wikipedia mentions a system at http://en.wikipedia.org/wiki/Hoare_logic called Hoare logic which was designed "to reason about the correctness of computer programs with the rigour of mathematical logic". --WEC