Gödel proof code applet
| Some related reading |
|---|
| 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:
The proofs are encoded based on the following table:
| End of proof | 00 | |
| 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 WF | 0111 |
| I1 | x=y⇒(x=z⇒y=z) | 0001 |
| I2 | x=y⇒x'=y' | 0011 |
| I3 | ¬0=x' | 0101 |
| I4 | x'=y'⇒x=y | 0111 |
| I5 | x+0=x | 1001 |
| I6 | x+y'=(x+y)' | 1011 |
| I7 | x*0=0 | 1101 |
| I8 | x*y'=(x*y)+x | 1111 |
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
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 |