Gödel numbering
The second stage in the proof is to use the Gödel numbering, described above, to show that the notion of provability can be expressed within the formal language of the theory. Suppose the theory has deduction rules: . Let be their corresponding relations, as described above.