 It is noteworthy that ω-consistency is not needed in the proof of Gödel’s Second Incompleteness Theorem. Also note that neither is ¬Con(P) provable, by the consistency of P and the fact, now known as Löb’s theorem, that P ⊢ Prov(⌈φ⌉) implies P ⊢ φ.