Gödel's incompleteness theorem - project summary

My Gödel's incompleteness theorem project has now produced an undecidable statement, and on this page there is a brief summary of how the project has gone, and what it might lead to in the future. The first thing to note is that the undecidable statement produced is a lot shorter than I thought it might be. When I started I had in mind a compiler which might produce a program of hundreds of kilobytes in length. I would then have to convert this into an arithmetical statement, and this might well have produced hundreds of characters for each byte of the program, leading to a statement of over a hundred megabytes. What made things a lot simpler was realising how suitable the programming language Haskell was for the task. The pure functional nature of Haskell made it very similar to the arithmetical formulae that it was to be converted too, and so this great expansion of the program did not occur.

I have to say here that I am not an expert in mathematical logic, and there might be something that I have overlooked that means that what I have done is not valid, and so that the sentence produced is not undecidable. Alternatively there might be a bug in the programs I have written (but that would be easier to patch up). The main area that I intend to look at is whether there will be any problems due to using a bit shifting method to define the Gödel numbering rather than Gödel's method based upon the prime decomposition of numbers. The reason that I will focus on this is that in Computability and logic by Boolos, Burgess and Jeffrey, a positional numbering method is considered, but rejected in favour of the prime number method. On the other hand, I feel that the method I have used is fairly persuasive, and so is probably OK.

There are certainly plenty of ways in which this project can be continued. I intend to tidy up and document the code,in particular to describe what parts of Haskell the conversion applet will accept. Apart from that, I've listed several ideas below. However, I'm not sure that I'll carry these out - for one thing I've got plenty of other stuff to do, but it also struck me that most of these would make an ideal project for a computer science undergraduate. If you plan to do any of these then do let me know.

The conversion applet at present only accepts a very limited subset of Haskell. In particular it doesn't do any of the pattern matching which is really the essence of Haskell. This is because the limited subset was all that was needed to carry out the project, but adding such pattern matching shouldn't be too much of a problem, at least as far as generating the output is concerned - the mechanics of the pattern matching is technial, but is present in existing Haskell compilers.

I wrote the conversion program in Java because I was reasonably familiar with the language, and it provides a straightforward way of putting it on to a website. However, there are programming languages which are more suited to writing such 'compiler-like' programs, in particular Haskell itself - Haskell compilers are generally written in Haskell.

When I started the project I wanted to keep the programs as simple as possible. Hence I chose a form of the arithmetical axioms with the least number of symbols. This meant, however, that expressions involving the symbols ∃ ∧ and ∨ had to be converted into ones just using ∀ and ⇒, which rather disguised what was going on. If I was starting again, I would definitely include ∃ ∧ and ∨ even though this would involve more axioms to define the relationships between the symbols.

Gödel's incompleteness theorem isn't the only important theorem of mathematical logic - there are plenty of related results, which would benefit from a similar project to actually produce statements that are shown to exist.

One thing that struck me when I was writing and testing the conversion program was that it involved a lot of working out by hand what a result should be and checking that the program agreed with this. So why not do the whole thing by hand? - it probably wouldn't have taken any longer. Also, there would be the possibility to introduce abbreviations in the rather long winded undecidable statement, and so end up with something that could be written in an even shorter way.