"?>

# Gödel proof code applet

In this book Torkel Franzen examines various ways that this theorem has been wrongly quoted, and tries to set the reader straight on what it is really about. He looks at what has been said about incompleteness in physics, in theology and of course in various postmodern ramblings.

My review of Godel's theorem : an incomplete guide to its use and abuse
This is an applet to implement a numerical encoding of arithmetical proofs, as is required in the proof of Gödel's incompleteness theorem. It uses the axiom system describes in A proof system for arithmetic. I you look at the proof in A formal proof that 1+1=2, you will see that the second column is what is normally considered to be the proof - a sequence of arithmetical statements. This encoding however, is based on what is in the third column - a description of the axiom used, with parameters as required. These descriptions can then be used to build the sequence of statements in the second column.
The proofs are encoded based on the following table:

End of proof00
Ax1(WF1,WF2)WF1⇒(WF2⇒WF1)0001
Ax2(WF1,WF2,WF3)(WF1⇒(WF2⇒WF3))⇒((WF1⇒WF2)⇒(WF1⇒WF3))
0101
Ax3(WF1,WF2)(¬WF2⇒¬WF1)⇒((¬WF2⇒WF1)⇒WF2)1001
Ax4(V,T,WF)∀V WF(V)⇒WF(T)
##### (T is a term free for V in WF)
0010
Ax5(V,WF1,WF2)∀V(WF1⇒WF2)⇒(WF1⇒∀V WF2)
##### WF1 has no free occurence of V
0110
Ind(V,WF) WF(0) ⇒((∀V (WF(V) ⇒ WF(V'))) ⇒ ∀V WF(V))1010
MP(l1,l2) WF1,WF1 ⇒ WF2 |- WF2 0011
Gen(V,l1)WF |- ∀V WF0111
I1x=y⇒(x=z⇒y=z)0001
I2x=y⇒x'=y'0011
I3¬0=x'0101
I4x'=y'⇒x=y0111
I5x+0=x1001
I6x+y'=(x+y)'1011
I7x*0=01101
I8x*y'=(x*y)+x1111

The formulae, variables and terms in the proofs are encoded using the scheme described in Gödel numbering applet. As with that page, the encoding uses a reverse polish encoding, and progresses from the least significant bit of the number. The applet thus takes a number representing the sequence of axioms used, and outputs a list of numbers representing the statements proved (using the encoding in Gödel numbering applet).

I realise that this is likely to be confusing, so the best thing to do is to try it out. Copy the number from the the proof.txt file into the top box, and press the down button.
###### I would have put the number on this page - its less than 500 digits - but it needs to be all in one piece and so won't wrap on the page.

A sequence of numbers will appear in the lower box. Copy these to the applet on the Gödel numbering applet page and use that to generate a sequence of statements. This should end with (0'+0')=0'', which is the same as 1+1=2. The statements will reproduce the proof given on the page A formal proof that 1+1=2

 You do not appear to have Java enabled on this browser. (Note that Java is no longer supplied by default on Windows systems). The latest Java environment can be downloaded and installed from the Java website

I recognise that these applets are a bit clumsy at the moment, (it took several days work to create the encoding for the proof of 1+1=2). I hope to improve them as time goes on. But the important part isn't so much using them, it's the existence of a function which can translate and encoded form of a proof into an encoded form of the statement to be proved. This will be used in generating an undecidable statement.

 Source code Source code Licence