Gödel proves that a formal system containing arithmetic must be incomplete (i.e. incapable of proving all true statements). The proof consists in creating a statement that says "this statement cannot be proved", for then it follows that either this this statement can be proved and we have proved something false, or it cannot be proved but it is still true. In either case our formal system is flawed. This is in a way an instance of the liar paradox, which was of course well know long before, but no-one had expected it to materialise inside a seemingly sensible formal system. Gödel shows that it does by means of his arithmetisation trick that enables the system to speak about itself. All symbols in the system's alphabet is given a unique number. Then all formulas in the system is assigned the following number: the product of all the factors (n:th prime)^(n:th symbol in the formula). By unique prime factorisation one can recreate the formula from its number. Sequences of formulas---proofs in particular---can be coded by the same method. We can now express the relation "x is a proof of y" inside the formal system. This relation takes two arguments: x*, the Gödel number for the sequence of formulas x, and y*, the Gödel number for the formula y. Inside the formal system it is a perfectly well defined and finite problem to decide whether x is a proof of y, as is quite plausible, although Gödel has to work hard with his recursion theory to prove this strictly. Now that we can express "x is a proof of y" we can also express "x is a proof of y(z)", i.e. a relation that takes three arguments: x*, y*, z*, the Gödel numbers for a sequence x of formulas, a formula y with a free variable, and a formula z. Thus we can also express "there exists no x such that x is a proof of y(z)". In particular, we can send in y* for z, and the statement becomes: "there exists no x such that x is a proof of y(y*)". This expression has one free variable, y. Call it F(y). F(y) is a formula in our formal system, so it has a Gödel number, say F*. Now we can formulate the statement "this statement cannot be proved" inside our formal system as follows: "F(F*)"="there exists no x such that x is a proof of F(F*)"="F(F*) cannot be proved". So if our formal system is consistent (i.e. does not prove false things) then we must accept that it cannot prove F(F*), but then F(F*) is true, so our formal system is incomplete.