Gödel's incompleteness theorem
|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
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
Putting it all together