>> Then Gödel shows up and says, "On which shelf shall we put the index?"
> You keep it outside the library. The index tells you where every single book is, other than the index.
This approach would have saved Russell and Whitehead's "Principia Mathematica" project, would have placed mathematics on a firm foundation, but it suffers from the same defect of self-reference -- it places the index beyond validation. Russell realized this, and recognized that Gödel's results invalidated his project.
> The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct;
Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
Quote: "Gödel hammered the final nail home by being able to demonstrate that any consistent system of axioms would contain theorems which could not be proven. Even if new axioms were created to handle these situations this would, of necessity, create new theorems which could not be proven. There's just no way to beat the system. Thus he not only demolished the basis for Russell and Whitehead's work--that all mathematical theorems can be proven with a consistent set of axioms--but he also showed that no such system could be created." (emphasis added)
> Russell realized this, and recognized that Gödel's results invalidated his project.
One particular project. The specific project of formalizing mathematics within itself is unachievable. That doesn't mean we've stopped doing math.
And this is in fact the approach modern mathematics has taken. The fact that one particular book (the proof of mathematics' own consistency) can't be found on the shelves doesn't mean there isn't value in keeping the rest of the books well-organized.
> Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
No! Humans aren't developed in either Coq or ML. A human can look at Coq and say "Yes, this is correct" or "No, this is wrong" just fine, without running afoul of the halting problem, Gödel's incompleteness theorem, or anything else. The fact that you can have no Coq-proven confidence in Coq's correctness does not mean that you can have no confidence of Coq's correctness.
(Of course, this brings up whether a human should be confident in their own judgments, but that's a completely unavoidable problem and rapidly moving to the realm of philosophy. If you are arguing that a human should not believe anything they can convince themselves of, well, okay, but I'm not sure how you plan to live life.)
This is like claiming that, because ZF isn't provably correct in ZF (which was what Russell, Whitehead, Gödel, etc. were concerned about -- not software engineering), mathematicians have no business claiming they proved anything. Of course they've proven things just fine if they're able to convince other human mathematicians that they've proven things.
>> Russell realized this, and recognized that Gödel's results invalidated his project.
> One particular project.
A mathematical proof applies to all cases, not just one. Gödel's result addressed Russell's project, but it applies universally, as do all valid mathematical results. Many mathematicians regard Gödel's result as the most important mathematical finding of the 20th century.
> That doesn't mean we've stopped doing math.
Not the topic.
> A human can look at Coq and say "Yes, this is correct" or "No, this is wrong" just fine, without running afoul of the halting problem, Gödel's incompleteness theorem, or anything else.
This is false. If the Halting problem is insoluble, it is also insoluble to a human, and perhaps more so, given our tendency to ignore strictly logical reasoning. It places firm limits on what we can claim to have proven. Surely you aren't asserting that human thought transcends the limits of logic and mathematics?
> Of course they've proven things just fine if they're able to convince other human mathematicians that they've proven things.
Yes, with the caution that the system they're using (and any such system) has well-established limitations as to what can be proven. You may not be aware that some problems have been located that validate Gödel's result by being ... how shall I put this ... provably unprovable. The Turing Halting problem is only one of them, there are others.
> A mathematical proof applies to all cases, not just one. Gödel's result addressed Russell's project, but it applies universally, as do all valid mathematical results.
What? I have no idea what you mean by "applies universally" and "all valid mathematical results."
A straightforward reading of that sentence implies that Pythagoras' Theorem is not a "valid mathematical result" because it applies only to right triangles. That can't be what you're saying, is it?
I am acknowledging that Gödel's second theorem states that any mathematical system that attempts to prove itself is doomed to failure. I am also stating that Russell's project involved a mathematical system that attempts to prove itself. Therefore, Gödel's second theorem applies to Russell's project, but it does not necessarily say anything else about other projects.
> Many mathematicians regard Gödel's result as the most important mathematical finding of the 20th century.
So what? This is argumentum ad populum. How important the mathematical finding is is irrelevant to whether it matters to the discussion at hand.
> This is false. If the Halting problem is insoluble, it is also insoluble to a human
OK, so do you believe that modern mathematics is invalid because Russell's project failed?
> You keep it outside the library. The index tells you where every single book is, other than the index.
This approach would have saved Russell and Whitehead's "Principia Mathematica" project, would have placed mathematics on a firm foundation, but it suffers from the same defect of self-reference -- it places the index beyond validation. Russell realized this, and recognized that Gödel's results invalidated his project.
> The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct;
Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
Source: http://www.sscc.edu/home/jdavidso/math/goedel.html
Quote: "Gödel hammered the final nail home by being able to demonstrate that any consistent system of axioms would contain theorems which could not be proven. Even if new axioms were created to handle these situations this would, of necessity, create new theorems which could not be proven. There's just no way to beat the system. Thus he not only demolished the basis for Russell and Whitehead's work--that all mathematical theorems can be proven with a consistent set of axioms--but he also showed that no such system could be created." (emphasis added)