 Proof: Let φ be as in (3). The reasoning used to infer ‘if P ⊢ φ, then P ⊢ 0 ≠ 1‘ does not go beyond elementary number theory, and can therefore, albeit with a lot of effort (see below), be formalized in P. This yields: P ⊢ (Prov(⌈φ⌉) → ¬Con(P)), and thus by (3), P ⊢ (Con(P) → φ). Since P ⊬ φ, we must have P ⊬ Con(P).