A formal proof of Godel's Incompleteness Theorem?

### A formal proof of Godel's Incompleteness Theorem?

•andrewk
Inexhaustibly Curious Usergroup: Moderators Joined: Oct 13, 2011 Location: Sydney, Australia Total Topics: 47 Total Posts: 5840 Last Blog: The Joys of VERY Amateur Music |
Posted Oct 5, 2012 - 7:20 PM:
Subject: A formal proof of Godel's Incompleteness Theorem? I am contemplating embarking on a project of trying to write an approachable yet formal proof of Godel's first incompleteness theorem. This result is, like Relativity and some aspects of quantum mechanics, one of the most commonly referenced aspects of difficult mathematics and science in popular discussion, yet very few people understand the proof. That includes me. I learned about Godel's result about thirty years ago in a popular maths book that included an informal proof sketch, and I have reflected on it occasionally on and off since then. But until a couple of weeks ago I had never tried to work my way through a rigorous proof. Hofstadter's "Godel Escher Bach" has a semi-rigorous exposition of it, but he takes a few hundred pages to do it, which makes it hard to keep track of what is actually part of the proof and what is colourful background or tangents, what with Zen koans, hares, torotoises and such-like. A few weeks ago I did some internet searching for proofs. Nearly everything that comes up is proof sketches rather than rigorous. I didn't find Godel's original paper, but I was discouraged from looking further anyway because I can't understand German and what I found suggested that most translations of the proof were poor. Also, unless Godel was an especially lucid writer, there's no reason to suppose his original proof is especially approachable. It's also likely that he skips plenty of steps, as that is regrettably the usual fashion in academic papers. The best one I found was some lecture notes by B.Kim at http://web.yonsei.ac.kr/bkim/goedel.pdf, entitled "Complete proofs of Godel's Incompleteness Theorems." These are quite good, and more rigorous than anything else I've seen. However they contain a number of errors, do not accompany many formal steps with intuitive explanations of why the step is being taken, and use notation that makes it difficult to keep track of what is reasoning So, largely for my own benefit, I am thinking of attempting to write a proof, based on Kim's notes, but using clearer notation, providing intuitive explanations, filling in missing steps, and using colour coding or some other device (yet to to be determined) to distinguish the different types of reasoning. One payoff from doing this, but by no means the only one, would be that it would make it easy to point to a step in which it is reasoning from outside the system in a way that could not have been done inside the system, and why the step is nevertheless valid. I am hoping this will enable a better intuitive sense of what "enlarging the system to enable a proof that the statement is true" would involve, and why that is futile because there will then be another statement that is true but unprovable in the enlarged system. The sites I've looked at that discuss this talk about enlarging the system just by adding an axiom stating that the key statement is true, which I find deeply unsatisfying. An enlargement such as moving to a higher order of logic would be much more convincing. So now to my question: Has anybody come across a proof of the first Incompleteness Theorem that already has these features, and if so can you point me to it? If it already exists, I would be wasting my time trying to create one. I could just read that one and enjoy it and the more intuitive understanding that would flow from it. |

•MoeBlee
aka I. Kabruob Usergroup: Members Joined: May 19, 2005 Total Topics: 10 Total Posts: 702 |
Posted Oct 5, 2012 - 10:22 PM:
andrewk wrote: I don't know about a text that has all the features you seek, but just about any introductory textbook has a proof of the Godel-Rosser incompleteness theorem. Some books have more detail than others. I would recommend Enderton's 'A Mathematical Introduction To Logic'. There are some gaps where you'd have to fill in some details, but you can take such gaps as excercises ranging from easy to somewhat challenging.Has anybody come across a proof of the first Incompleteness Theorem that already has these features P.S. As to "inside the system" vs. "outside the system", you'll find that Enderton's text will allow you to be clear at each point. |

•timw
PF Addict Usergroup: Members Joined: Nov 14, 2008 Total Topics: 39 Total Posts: 1159 |
Posted Oct 6, 2012 - 3:56 PM:
Godel's 1931 paper (in English, for me) is readable and literate! Try that. |

•Rilx
Resident Usergroup: Sponsors Joined: Jan 16, 2009 Location: Finland Total Topics: 2 Total Posts: 205 ♂ |
Posted Oct 6, 2012 - 4:50 PM:
The original name is: (Über formal unentscheidbare Sätze der Google, and ye shall find. |

•andrewk
Inexhaustibly Curious Usergroup: Moderators Joined: Oct 13, 2011 Location: Sydney, Australia Total Topics: 47 Total Posts: 5840 Last Blog: The Joys of VERY Amateur Music |
Posted Oct 6, 2012 - 9:14 PM:
Rilx wrote: On Formally Undecidable Propositions of Principia Mathematica and Related SystemsGood thinking! For some reason I didn't consider googling the English translation of the full title. Instead I was googling things like "godel incompleteness theorem english proof". As soon as I tried your way I came up with some very promising links, including the following translation: www.research.ibm.com/people.../papers/canon00-goedel.pdf I am now a little torn. Having invested a week or so in working through Kim's proof (with interruptions), I'm a little reluctant to incur all the overheads of learning a new notation and set of lemmas, in order to get through Godel's version. The intro in the IBM version above says one problem is that the original paper is written in notation that has mostly fallen into disuse. I think the IBM people have updated the notation, but I haven't yet looked to see how thoroughly. I think I had better read the IBM version though. Given that my question is whether to bother writing a formal, clear, accessible proof, and I know the Kim version doesn't quite meet those (unrealistically high) standards, I should first check whether the great man's own version does. I think I'll order the Enderton book MoeBlee mentioned, as I don't currently have any books dealing with formal logic. But given they take weeks to arrive from Amazon, and I'm an impatient sod, I'll probably have either started a proof by then or (more likely) got distracted by some new, shinier bauble by the time it arrives. |

•throng
Profester. Usergroup: Members Joined: Aug 12, 2008 Location: Downunder. Total Topics: 65 Total Posts: 1196 ♂ |
Posted Oct 7, 2012 - 12:56 AM:
Isn't it paradoxial to formally prove that theorum? |

•andrewk
Inexhaustibly Curious Usergroup: Moderators Joined: Oct 13, 2011 Location: Sydney, Australia Total Topics: 47 Total Posts: 5840 Last Blog: The Joys of VERY Amateur Music |
Posted Oct 7, 2012 - 2:36 AM:
throng wrote: No. The theorem proves that, given a formal language L and a theory T in that language that includes Peano Arithmetic and certain logical axioms, then, providing T is consistent, there exists a sentence (ie a proposition) S in the language L that is true but cannot be proven by the methods available within L and T. Isn't it paradoxical to formally prove that theorum? The theorem proves both the truth and the unprovability by arguing from outside the theory T. That is, the methods of argument available are greater than those available within T. So there is no contradiction. The theorem said S can't be proven within T, and we had to go However, it is critical to a sound understanding of this to be clear about what methods of argument used in proving the theorem are not available within T, and proofs I have read so far lack precision on this critical issue. The proof contains quantification over formulas, which is a second-order operation, not available within first order predicate logic. But there may be more to it than that. Further, I think Godel's result applies equally to a T that is second-order or higher, in which case quantification over formulas is allowed witin T. |

•Willemien
Blond Dutch Mensa meisje Usergroup: Sponsors Joined: Apr 05, 2011 Location: London (UK) Total Topics: 77 Total Posts: 1284 ♀ |
Posted Oct 7, 2012 - 2:32 PM:
I am wondering if anybody ever wrote a complete proof of Godels incompleteness theorem. Godel only wrote how to build a proof of his theorems, not an actual complete proof and I think others are almost inevitable doing the same, a complete proof is just tedious and unnescesary. But if you really want I think to write a complete proof it is best to change the whole proof to Polish notation (less symbols so less big numbers) but even then, i once heard that the smallest godel number just fitted onn an A4 sheet of paper, not sure if that was just jest or if they really calculated one. not sure about your remark: The proof contains quantification over formulas. I thought it was mostly converting formula's to numbers and doing operations on the numbers, so you aren't quantifyiong over formula's but over numbers What i think is a good book about it is An Introduction to Godels Theorems by Peter Smith 360 pages on the theorems but no proof, I read on his website that he is working on a further book on it so maybe wiait for that. (but again don't expect a complete proof) |

•andrewk
Inexhaustibly Curious Usergroup: Moderators Joined: Oct 13, 2011 Location: Sydney, Australia Total Topics: 47 Total Posts: 5840 Last Blog: The Joys of VERY Amateur Music |
Posted Oct 7, 2012 - 5:18 PM:
Most Godel numbers are unimaginably huge, it's true. But they're not all huge. Edited by andrewk on Oct 8, 2012 - 9:30 PM |

•andrewk
Inexhaustibly Curious Usergroup: Moderators Joined: Oct 13, 2011 Location: Sydney, Australia Total Topics: 47 Total Posts: 5840 Last Blog: The Joys of VERY Amateur Music |
Posted Oct 8, 2012 - 9:28 PM:
I have written a little R script to calculate Godel numbers. Willemien is right. The numbers do get horribly huge with alarming alacrity. I have however, with about half an hour of computer time, managed to ascertain that the formula "0=0" has Godel number: 7,286,659, if we map the language symbols '0' and '=' to 0 and 1 respectively. The smallest Godel number I could get for a complete well-formed formula was 865 for the formula 'P0' where P is the symbol for a unary predicate and the language symbols '0' and 'P' are mapped to 0 and 1 respectively. P can mean whatever we wish to define it to mean. So if we define P(x) to mean x=0 then 'P0' has an encoding of '0=0' with a much smaller Godel number. |

### Recent Internal Replies

On Nov 2, 2012 - 6:15 PM, Mystermenace replied internally to Mystermenace's As you noted, Gode.... | |

On Nov 1, 2012 - 10:11 PM, andrewk replied internally to Mystermenace's As you noted, Gode.... | |

On Nov 1, 2012 - 9:02 PM, Mystermenace replied internally to Mystermenace's As you noted, Gode.... | |

On Nov 1, 2012 - 8:03 PM, andrewk replied internally to Mystermenace's As you noted, Gode.... | |

On Nov 1, 2012 - 5:12 PM, andrewk replied internally to MoeBlee's I hope later to have.... | |

On Oct 17, 2012 - 8:34 PM, andrewk replied internally to MoeBlee's The necessary proper.... | |

On Oct 10, 2012 - 5:09 PM, andrewk replied internally to MoeBlee's (1) Godel's own .... |

This thread is closed, so you cannot post a reply.