# A formal proof of Godel's Incompleteness Theorem?

andrewk
Inexhaustibly Curious

Usergroup: Moderators
Joined: Oct 13, 2011
Location: Sydney, Australia

Total Topics: 46
Total Posts: 5046

Last Blog: Authentically engaging with the world

#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: 352
#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 features
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.

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
Forum Veteran

Usergroup: Members
Joined: Nov 14, 2008

Total Topics: 33
Total Posts: 842
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

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: 46
Total Posts: 5046

Last Blog: Authentically engaging with the world

#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: 59
Total Posts: 1153
#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: 46
Total Posts: 5046

Last Blog: Authentically engaging with the world

#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

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.

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: 46
Total Posts: 5046

Last Blog: Authentically engaging with the world

#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: 46
Total Posts: 5046

Last Blog: Authentically engaging with the world

#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.
This inactive thread has been archived. To continue the topic, start a new one.
• 100/5
• 1
• 2
• 3
• 4
• 5

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.