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
A formal proof that 1+1=2
Gödel proof code applet
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 arithmetization applet
Gödel's fixed point theorem