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.


  • [Snapshot]
  • [Snapshot]
  • [Snapshot]


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 .
    • Share:

Embed Interactive Demonstration New!

Just copy and paste this snippet of JavaScript code into your website or blog to put the live Demonstration on your site. More details »

Files require Wolfram CDF Player or Mathematica.