Gödelization

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
Snapshots
Details
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 .
Permanent Citation