Dan: What you are describing is the whole Hilbert/Russell program, which was derailed to some extent by Goedel. However, the absence of a finite set of axioms for mathematics doesn't mean the end of proper proofs. Look how much math today depends upon the Riemann Hypothesis, the Axiom of Choice, etc. Unfortunately, we don't even have a proper proof-checker for high school plane geometry (that in itself would be a good thing, so that high school students could check their own work). (High school plane geometry is decidable, as it is reducible to the theory of Real Closed Fields, but the general decision process is multiply-exponential, and hence currently not practical. But a decision procedure isn't necessary to verify a proof -- only to find one.) At 10:15 AM 3/3/2006, dasimov@earthlink.net wrote:
Gene wrote re proof-checking software:
<< 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?
It seems possible there could be a bootstrap method to create perfect proof-checking software (I suspect this has already been done for plane geometry), but in general this would rely on the mathematics in question having been axiomatized. Axiomatizing all of math is one of the biggest obstacles to having a universal proof-checker lies. The other is translating putative math proofs, often written largely in natural language, into putative symbolic proofs.
If a putative proof is then put into official proof format, as defined by logicians, then -- assuming sufficient computing resources -- checking it should be a piece of cake. (Each statement in sequence must be either
1) an axiom or
2) a statement B such that statements A, and A => B, are prior statements in the proof,
and the last statement is what was to be proved.)
There is also the question of the consistency of the axioms, and imo especially those of set theory/category theory. E.g., since there can't be a set of all sets, I have to question the meaning of the "class of all sets" -- a "concept" that is dubious at best.
--Dan