 The next essential step of Gödel’s proof is to take the language of a formal system, which is always precisely defined (this is part of being a formal system), and fix a correspondence of a certain kind between the expressions of that language and the system of natural numbers—a coding, “arithmetization”, or “Gödel numbering”, of the language. There are many possible ways of accomplishing this, and the details do not really matter (for some more details of one quite standard approach, see the supplementary document  Gödel Numbering).  The essential point is that the chosen mapping is effective: it is always possible to pass, purely mechanically, from an expression to its code number, and from a number to the corresponding expression. Today, when most of us are familiar with computers and the fact that so many things can be coded by zeros and ones, the possibility of such an arithmetization is hardly surprising.