Return to Revisions

For the philosophical point encapsulated in (*) in the question, it seems that corollaries of the second incompleteness theorem are more relevant than the theorem itself. If we had doubts about the consistency of ZFC, then a proof of Con(ZFC) carried out in ZFC would indeed be of little use. But a proof of Con(ZFC) carried out in a more reliable system, like Peano arithmetic or primitive recursive arithmetic, would (before Gödel) have been useful, and I think this is what Hilbert was hoping for. Gödel's second incompleteness theorem tells us that this sort of thing can't happen (unless even the more reliable system is inconsistent).