# 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. |

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

Bits | Formula | |
---|---|---|

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

Bits | Expression | |
---|---|---|

0 | variable | |

001 | 0 | constant |

011 | term' | 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.

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).