### 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 #1 - Quote - Permalink 1 of 1 people found this post helpful 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 inside the system and what is outside it, reasoning about the system. 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 #2 - Quote - Permalink Posted Oct 5, 2012 - 10:22 PM: andrewk wrote:Has anybody come across a proof of the first Incompleteness Theorem that already has these featuresI 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.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 •timw #3 - Quote - Permalink 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 ♂ •Rilx #4 - Quote - Permalink Posted Oct 6, 2012 - 4:50 PM: The original name is: On Formally Undecidable Propositions of Principia Mathematica and Related Systems (Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme) 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 #5 - Quote - Permalink Posted Oct 6, 2012 - 9:14 PM: Rilx wrote:On Formally Undecidable Propositions of Principia Mathematica and Related Systems Good 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 ♂ #6 - Quote - Permalink 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 #7 - Quote - Permalink Posted Oct 7, 2012 - 2:36 AM: throng wrote:Isn't it paradoxical to formally prove that theorum?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. 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 outside T to prove it. 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 ♀ #8 - Quote - Permalink 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 #9 - Quote - Permalink Posted Oct 7, 2012 - 5:18 PM: Most Godel numbers are unimaginably huge, it's true. But they're not all huge. '0' is a term to which a Godel number must be assigned, and if we assign the number 1 to the symbol '0' in our chosen formal language then the Godel number of the term '0' is 21 = 2 using Godel's prime factors approach to encoding (Kim uses a different encoding approach that produces smaller numbers, but Godel's is easier to understand). 'x->x' is a very short well-formed formula [ETA: no it's not. A variable like x cannot represent a formula in first-order logic], that also happens to be a tautology. If we assign the Godel numbers 2 and 3 to the symbols 'x' and '->' then the Godel number of this formula is 223352 = 13,500. [ETA This is wrong. I misused the encoding algorithm. It's more complex than that and will probably give a much bigger number. I'll try to work it out and then re-post. I hope it fits on a page!] One of the most critical steps in Godel's proof, the 'Fixed Point Theorem' (aka 'Diagonal Lemma'), uses the fact that a certain formula exists in the language with special properties. Formally expressed, this is $$\exists \phi (F(\phi))$$ where $$\phi$$ is a well-formed formula in the formal language L, and F is another well-formed formula in L that contains $$\phi$$ as a subformula, perhaps with some variable substitutions therein. This is existential quantification over formulas of L, which appears to be a second-order activity. In fact, even the statement of Godel's theorem, in many of its forms, seems to require existential quantification: in words saying there exists a formula in L that is true but not provable. Sorry about all the spaces. Mathjax is really misbehaving this morning. It doesn't seem to like phi. 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 #10 - Quote - Permalink 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.