 Informally, the reasoning leading to the second incompleteness theorem is relatively simple. Given the arithmetized provability predicate, it is also easy to present an arithmetized consistency statement: pick some manifestly inconsistent formula (in arithmetical theories, a standard choice is \((\underline{0} = \underline{1})\)); let us denote it by \(\bot\); (the arithmetized counterpart of) the consistency of the system can then be defined as \(\neg\Prov_F (\ulcorner \bot \urcorner)\). Let us abbreviate this formula by \(\Cons(F)\). The proof of the first part of the first incompleteness theorem (i.e., the case (i) above) can then presumably be formalized inside \(F\) (in practice this would certainly be intricate). This gives: