From Academic Kids

In formal number theory a Gödel numbering is a function which assigns to each symbol and formula of some formal language a unique natural number called a Gödel number (GN). The concept was first used by Kurt Gödel for the proof of his incompleteness theorem.
Contents 
Definition
Given a countable set S, a Gödel numbering is a function
 <math>f:S \to \mathbb{N}<math>
with both f and the inverse of f a computable function.
Example
Step 1
Gödel numbers are constructed with reference to symbols of the propositional calculus and formal arithmetic. Each symbol is first assigned a natural number, thus:
Logical symbols  Numbers 1:12  

¬ 
1 ("not")  
Propositional symbols  Numbers greater than 10 but divisible by 3  
P 
12 

Individual variables  numbers greater than 10 with remainder 1 when divided by 3  
v 
13 

Predicate symbols  numbers greater than 10 with remainder 2 when divided by 3  
E 
14 
And so on and so forth (NB the syntax of the propositional calculus ensures that there is no ambiguity between "P" and "+", even though both are assigned the number 12).
Step 2
Arithmetical statements are assigned unique Gödel numbers referenced to the series of prime numbers. This is based on a simple code which essentially reads
prime 1 ^{character 1} * prime 2 ^{character 2} * prime 3 ^{character 3}
and so on.
For example the statement
<math>\forall<math>x, P(x) becomes
2^{2} * 3^{16} * 5^{12} * 7^{6} * 11^{16} * 13^{7}, because
{2, 3, 5, 7, 11, ...} is the prime series, and 2, 16, 12, 6, 16, 7 are the relevant character codes. This is a large but perfectly determinate number (namely 14259844433335185664666562849653536301757812500).
Step 3
Finally, sequences of arithmetical statements are assigned further Gödel numbers, such that the sequence
Statement 1 (GN1)
Statement 2 (GN2)
Statement 3 (GN3)
gets the Gödel number 2^{GN1}*3^{GN2}*5^{GN3}, which we will call GN4. The proof of Gödel's incompleteness theorem depends on the demonstration that, in formal arithmetic, some sets of statements logically entail or prove other statements. For example it might be shown that GN1, GN2, and GN3 together, i.e. GN4, prove GN5. Because this is a demonstrable relationship between numbers it is entitled to its own symbol, for example R. Then we could write R(v,x) to express "x proves v". In the case where x and v are Gödel numbers GN4 and GN5 we would say R(GN5,GN4).
An informal account of the proof
The core of Gödel's argument is that we can write the statement
 <math>\forall<math>x, ¬R(v,x)
which means
 no proposition of type v can be proved.
The Gödel number for this statement would be
 2^{2} * 3^{16} * 5^{1} * 7^{18} * 11^{6} * 13^{12} * 17^{16} * 19^{7}
but we will call it GN6. Now if we consider the statement
 <math>\forall<math>x, ¬R(GN6,x),
we will realise that it says
 no proposition that says 'no proposition of type v can be proved' can be proved.
This collapses into the statement
 this proposition cannot be proved.
If the statement can actually be proved, then its formal system is inconsistent because it proves something which states that it itself cannot be proven (a contradiction). If the statement cannot be proved within its formal system, then what the statement asserts is actually true, so the statement is consistent, but since the formal system contains a statement which is semantically true but which cannot be proven (syntactically), then the system is incomplete. Therefore, assuming that the formal system is consistent, it has to be incomplete.
Discussion
The Gödel numbering is not unique. The general idea is to map formulas onto natural numbers. An alternative Gödel numbering could be to consider each of the symbols of Step 1 to be mapped (through, say, a mapping h) to a digit of a base22 numeral system, so a formula consisting of a string of n symbols <math> s_1 s_2 s_3 ... s_n<math> would be mapped to the number
 <math> h(s_1) \times 22^{(n1)} + h(s_2) \times 22^{(n2)} + ... + h(s_{n1}) \times 22^1 + h(s_n) \times 22^0. <math>
Also, Gödel numbering implies that each inference rule of the formal system can be expressed as a function of natural numbers. If f is the Gödel mapping and if formula C can be derived from formulas A and B through an inference rule r, i.e.
 <math> A, B \vdash_r C \ <math>,
then there should be some arithmetical function g_{r} of natural numbers such that
 <math> g_r(f(A),f(B)) = f(C). \ <math>
Then, since the formal system is a formal arithmetic, which can make statements about numbers and their arithmetical relationships to each other, it follows that the system can also, by means of Gödel coding, indirectly make statements about itself: that is, a proposition of the formal system can make assertions which, when viewed through the perspective of the Gödel mapping, translate into assertions about other propositions of the same formal system, or even about itself. Thus, by this means a formal arithmetic can make assertions about itself, becoming selfreferential, almost like a second order logic. This provided Gödel (and other logicians) with a means of exploring and discovering proofs about consistency and completeness properties of formal systems.
See also: Church number.
Further reading
 Gödel, Escher, Bach: an Eternal Golden Braid, by Douglas Hofstadter. This book defines and uses an alternative Gödel numbering.de:Gödelnummer