 Before proceeding to the details of the formal proof, we define the notion of ω-consistency used by Gödel in the First Incompleteness Theorem: P is ω-consistent if P ⊢ ¬φ(n) for all n implies P ⊬ ∃xφ(x). Naturally this implies consistency and follows from the assumption that the natural numbers satisfy the axioms of Peano arithmetic.