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 appletThe 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 σ1 button and the second by pressing the σ2 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.
|Source code Licence|
The Gödel2 program
- 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)