Gödel's incompleteness theorem
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 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 The Gödel number of the undecidable sentence The undecidable Gödel sentence Gödel's incompleteness theorem - project summary Javadoc Documentation of Applets Gödel arithmetization applet details Recommended Reading
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
