Gödel arithmetization applet

Some related reading
This isn't the easiest introduction to Gödel's work, but it sticks to the point rather than trying to deal with the whole of mathematical logic, and so provides a comprehensive treatment of Gödel's and related theorems in a concise book
My review of Gödel's incompleteness theorems

This is the program which carries out the most important part of this project, the conversion of a function (expressed as a computer program) into an arithmetical formula. It works very much like a compiler, you input a program written in a programming language, and it tranforms this program into another form. In this case, rather than producing executable output, it expresses the program in terms of the Gödel number of an arithmetical formula.

How to use the applet

The program which is processed by the applet is Godel2.hs - this is automatically loaded into the applet at the start. This is written in a limited subset of the Haskell programming language, which the applet processes. There are more details about this program below. What this applet does is to convert it to an arithmetical formula, and then, using the method described in Gödel's fixed point theorem to use this to generate an undecidable statement. On the Gödel's fixed point theorem page there are two ways of generating such a statement, the second being more general than the first. You can produce the first such statement by pressing the σ₁ button and the second by pressing the σ₂ button.

If you want to know what else you can do with the applet, well if you type in the name of one of the one parameter functions in the program into the edit box and press the y=*f*(x) button next to it then the applet will generate an arithmetic formula corresponding to that function. You can also type your own Haskell code into the applet, but you should note that it only processes a very limited subset of the language. I will give more details of the extent of this subset later, as well as looking into the facility to load and save files from the applet.

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

Source code

Source code Licence

Gödel's incompleteness theorem project

The Gödel2 program

The Gödel2 program is a proof checking program, and there is a java version of this program at Gödel proof code applet. You can test out this program if you like:

Download a Haskell implementation such as HUGS
Save the Godel2.hs file to your computer and load it into the Haskell environment
In the Haskell environment enter the contents of the proof1.txt file (This is the encoded form of my proof of 1+1=2)
The Haskell environment should give the answer 79059316. Copy this to the upper box in the Gödel numbering applet and press the down button to get the result 0'+ 0'=0'', (that is 1+1=2)