In 1931 Kurt Gödel established a representation between a formal system and the set of natural numbers to prove his famous incompleteness theorem. An axiom or a proof is encoded by assigning to each symbol in the expression odd numbers as the powers of successive primes. The expression can be recovered by factoring the number.
The coding scheme for typographic symbols is defined as follows:
The first six expressions correspond to the five Peano axioms for arithmetic (the third one has two parts). The other three are proofs that can be interpreted informally; the first is that the successor for 0 is 1; the second is that the successor of the successor of 0 is 2; the last is that .
![[Snapshot]](HTMLImages/index.en/thumbnail_1.gif)
![[Snapshot]](HTMLImages/index.en/thumbnail_2.gif)
![[Snapshot]](HTMLImages/index.en/thumbnail_3.gif)
Embed Interactive Demonstration 
Browse all topics
