"?>

Gödel numbering applet

Some related reading
John W Dawson has sifted through the massive amounts of paperwork that Gödel left, to produce this detailed but readable account of Gödel's life.
cover

My review of Logical dilemmas

This is an applet to implement a Gödel numbering scheme, that is to translate between formal arithmetic statements and positive integers.

To decode a number, the program starts with the low order bits and interprets them in terms of the following tables, using a reverse polish notation

BitsFormula
00 term = term equality
01 ¬ formula not
10 (formula1 formula2) implies
11 ∀ variable formula for all

When a term is being decoded the following table is used

BitsExpression
0variable
001 0 constant
011term' Successor function
101 (term + term) Addition
111 term * term Multiplication
Variables consist of a letter x,y,z which can followed by a numeric identifier. Variables are represented by a positive integer, which is obtained by taking the bits following the 0 two at a time and interpreting these in base 3, with 11 acting as a terminator.

The formula 0'+0'=0'' (that is 1+1=2) would be encoded as 100101101100101100101110100 in binary which is 79059316 in decimal notation

To use the applet you should enter a list of numbers into the upper box and then press the down button. The corresponding formulae will appear in the lower box. Alternatively enter a list of formulae into the lower box and press the up button, when they will be converted into code.


You do not appear to have Java enabled on this browser. (Note that Java is no longer supplied by default on Windows systems). The latest Java environment can be downloaded and installed from the Java website




To give you something to try the applet out on, the following numbers encode 8 axioms of integer arithmetic.

126178700386
473746530
14737
476254002
29140
1907082196
18908
15866905564

Source code
Source code Licence

Gödel's incompleteness theorem project


This applet has been updated, so that it can be used with the output of the undecidable statement generator. It now adds an extra high order bit when converting a formula, and requires this bit to be present when converting a number (otherwise it will signal an ERROR). Hence the numeric examples have been changed to reflect this. It also now has the check boxes to choose binary input, text-wrapping and html output (the html won't be valid in the other direction).