 The first incompleteness is proved for any such theory T, by explicitly producing an unprovable yet true statement \(G_\bT\). That formula can then be added to T making \(\bT+G_\bT\) a “less incomplete” theory. Von Neumann had already established the equivalence of \(G_\bT\) with the consistency statement for T, \(\Con (\bT)\); the latter expresses that there is no proof in T of a blatantly false statement such as \(0=1\). This gives then rise to an extension procedure leading from T to \(\bT'\), namely (R1) \(\bT'=\bT+G_\bT\).