(Thanks to Amit Sahai for spurring me to write this post!) The Background We all remember Gödel’s First Incompleteness Theorem from kindergarten.  This is the thing that, given a formal system F, constructs a sentence G(F) that’s a mathematical encoding of “This sentence is not provable in F.” If F proves G(F), then F proves both that F proves G(F) and that F doesn’t prove G(F), so F is inconsistent (and hence also unsound).  Meanwhile, if F proves Not(G(F)), then it “believes” there’s a proof o...