Gödel's incompleteness theorem
Recently Published |
---|
Hofstadter's latest book, in which he examines the parallels between Gödel's incompleteness theorem and the the emergence of mind |
My Review of I am a strange loop |
Gödel's incompleteness theorem states that given a first order axiomatization of arithmetic, such as the first-order Peano axioms, there exist arithmetical statements which cannot be either proved or disproved using those axioms. The aim of this project is to write a computer program which will generate such an undecidable statement from the axioms. This will be done in the following steps
Gödel numbering
The first part of Gödel's theorem is to devise a mapping between sequences of arithmetical statements and positive integers, giving the Gödel number of a sequence of such statements. In computer terms this looks simple - if a structure is stored on a computer then it will be stored as a sequence of bytes, and a sequence of bytes can be interpreted as a positive integer. However, it may turn out that a different mapping allows the rest of the proof to proceed more smoothly.
Applet implementing a Gödel numbering numbering scheme
Checking a proof via a computer
A proof of an arithmetical statement is a sequence of arithmetical statements, starting with the axioms and ending with the statement to be proved. Such a proof must follow fixed rules of inference. This means it is possible to write a boolean function PROVES(X,Y) where Y an arithmetical statement , and X is a possible proof of Y. This function returns true if X is a valid proof, and false otherwise. The intention is to produce such a program, written in a well-known programming language. However for what follows it may be more efficient to express it in a specially devised programming language as well.
A proof system for arithmetic
Unprovability expressed in terms of arithmetic
Arithmetical operations can be used to express the operations of a computer. Thus given a boolean function written for a computer, it is possible to translate it into an arithmetical statement. In particular we can transform the function PROVES(X,Y) into an arithmetical formula proves(x,y), where x and y are the Gödel numbers of X and Y. This transformation will be done in a similar way to that in which a programming language compiler would translate the code of PROVES(X,Y) into machine code.
Given the formula proves(x,y) we can then define unprovable(y) = ¬∃x(proves(x,y)), so we have a way of expressing the unprovability of arithmetical statements within arithmetic itself
Gödel's fixed point theorem
Given a formula with one free variable such as unprovable, the fixed point theorem (see for example http://math.yonsei.ac.kr/bkim/goedel.pdf ) shows how to construct an arithmetical statement Z with Gödel number z such that (Z⇔unprovable(z)) is a theorem of arithmetic. Then Z cannot be false, as this would mean that unprovable(z) is false, i.e. Z is provable and so true - a contradiction. Hence Z is true (so it cannot be proved false), meaning that unprovable(z) is true, which says that Z cannot be proved to be true. Thus Z is an undecidable statement, as required
The Gödel number of the undecidable sentence The undecidable Gödel sentence
Gödel's incompleteness theorem - project summary
Javadoc Documentation of Applets
Putting it all together