> > Gödel's Incompleteness Theorem: any sufficiently rich formal system, together with an interpretation, has strings which are true but unprovable.

Somewhat oddly, this is actually technically correct - a "sufficiently rich" system is one that can distinguish true versus false statements of Peano Arithmetic, and a inconsistent system, by the principle of explosion, can prove any statement, so cannot distinguish statements of Peano Arithmetic (eg, 1+1=2 and 1+1=3 are both provable), and hence is not sufficiently rich.

That's a somewhat unintuitive way of looking at it in practice, though.