 The Second Incompleteness Theorem establishes the unprovability, in number theory, of the consistency of number theory. First we have to write down a number-theoretic formula that expresses the consistency of the axioms. This is surprisingly simple. We just let Con(P) be the sentence ¬Prov(⌈0 = 1⌉).