 The above proof (sketch) of the Second Incompleteness Theorem is deceptively simple as it avoids the formalization. A rigorous proof would have to establish the proof of ‘if P ⊢ φ, then P ⊢ 0 ≠ 1’ in P.