In 1931, Gödel announced his striking incompleteness theorems, which assert that any reasonable formal system for mathematics is necessarily incomplete. In particular, if ZFC is consistent, then there are undecidable propositions in ZFC. Moreover, Gödel’s second incompleteness theorem implies that the formal (arithmetical) statement \(CON(ZFC)\), which asserts that ZFC is consistent, while true, cannot be proved in ZFC. And neither can its negation. Thus, \(CON(ZFC)\) is undecidable in ZFC.