Initializing live version
Download to Desktop

Requires a Wolfram Notebook System

Interact on desktop, mobile and cloud with the free Wolfram Player or other Wolfram Language products.

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.

Contributed by: Enrique Zeleny (March 2011)
Open content licensed under CC BY-NC-SA



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 .

Feedback (field required)
Email (field required) Name
Occupation Organization
Note: Your message & contact information may be shared with the author of any specific Demonstration for which you give feedback.