> The consistency of ZFC cannot be proven in ZFC - this follows from the second incompleteness theorem. The consistency of ZFC is a very useful theorem. Perhap

> The consistency of ZFC cannot be proven in ZFC - this follows from the second incompleteness theorem. The consistency of ZFC is a very useful theorem. Perhaps less useful than one might think. Given that an inconsistent system can prove anything, if you weren't convinced of ZFC's consistency to begin with I hardly think you'd be convinced by a proof of its consistency in itself. Godel's Second Incompleteness Theorem is important "in the other direction," that is its consequence for systems bigger than ZFC (or indeed PA)/larger statements that imply the consistency of your formal system in question. (A previous comment I made on this in greater detail https://news.ycombinator.com/item?id=25118038 https://news.ycombinator.com/item?id=25118038)