 Furthermore, by (4) and (2), we have P ⊢ ¬Prf(n, ⌈φ⌉) for all natural numbers n. By ω-consistency P ⊬ ∃x Prf(x, ⌈φ⌉). Thus (3) gives P ⊬ ¬φ. We have shown that if P is ω-consistent, then φ is independent of P.