Copyright © James R Meyer 2012 - 2017 www.jamesrmeyer.com
This is a step by step walk-through guide for anyone attempting to follow Gödel’s original proof of incompleteness, the paper entitled “On Formally Undecidable Propositions Of Principia Mathematica And Related Systems” (see online English translation of Gödel’s original proof or English translation of Gödel’s original proof, PDF file) . Despite the vast amount of material written about Gödel’s proof, I have not seen any good guide which actually takes the reader step by step through Gödel’s proof. There are a huge number of purported ‘explanations’ of Gödel’s proof, which claim to explain the proof, but do not actually follow Gödel’s actual proof, but instead use their own method. And while Gödel’s proof is constantly referred to with veneration, and has been called an “amazing intellectual symphony”, (Footnote: This accolade may be found in the section ‘The heart of Gödel’s argument (v)’ in the book Gödel’s Proof by E Nagel and J Newman. New York University Press, revised edition, 2001.
ISBN: 0814758169 Gödel’s Proof: Details.) the dearth of detailed analysis of the actual proof itself is all the more surprising. It is rather like telling musical students that Beethoven’s last String Quartet in F major is a masterpiece, and using a rewritten version to point out some facets of it, but at the same time refusing to actually analyze the actual details of the work itself to try and establish what makes it a masterpiece.
In addition, other authors seem to treat Gödel with an overwhelming reverence and treat Gödel’s paper as sacrosanct and above all criticism, so that anomalies in the proof are not mentioned, never mind questioned. While such anomalies will be noted, this will be done in order to assist the reader. In most cases the anomalies are inconsequential to the argument, but they can create real difficulties for someone reading the paper for the first time.
For this reason I decided to create a guide that leads the reader thorough the intricacies of Gödel’s proof, with the aim of being the best possible such guide to Gödel’s proof, which deals with the paper in a logical manner while at the same time explaining the line of argument of the proof. There is, of course, always room for improvement; if you have any suggestions or criticisms, contact me, they will be used to improve this guide. If there is any difficulty in following any part of the proof, please contact me and I will try to help.
It is only fair at this point to mention to the reader that this analysis reveals a fatal error in Gödel’s argument. However, this analysis is presented in an objective manner, and there is no attempt to mislead or deceive the reader, nor any attempt to conceal any aspect of the proof or to misrepresent any part of it. The intention is that by following this analysis, the reader will attain a better understanding of Gödel’s proof. I would note here that of all the incompleteness proofs I have examined, I much prefer Gödel’s, as its line of argument is much more subtle. And one cannot help but be impressed by Gödel’s virtuoso demonstration of how to translate meta-statements about formulas into number-theoretic relations about numbers. But a chain is only as strong as its weakest link, and if one is inspecting a chain to see if it is fit for purpose, one must look at every link, not just the shiny ones.
In this guide, we will not go into every single detail, but we will concentrate on those details that one needs to have a knowledge of in order to understand the line of argument in the proof. Once you understand how the proof works, then of course, you may want to look again at some aspects of the proof in more depth.
This guide is intended to be read alongside the English translation of Gödel’s original proof which can be viewed online at English translation of Gödel’s original proof or, if your browser is not displaying the symbols correctly, as a PDF at English translation of Gödel’s original proof, PDF. (Footnote: Alternative versions of Meltzer’s translation can also be found online Gödel’s Proof - Meltzer’s translation: here. Other translations of “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme” are available; one that is often referred to is one by Jean Van Heijenoort. It is not available online; it can be found in the book: From Frege to Gödel: A Source Book in Mathematical Logic, publisher: Harvard University Press, details From Frege to Gödel: A Source Book in Mathematical Logic: here. There are arguments as to which English translation is the ‘best’ and most faithful to the German original (which you can see Gödel’s original proof in German: here PDF), but the reality is that the differences between this translation and Meltzer’s are minor and inconsequential. Both of these use the same names for relations/functions as in Gödel’s original paper. Another English translation by Martin Hirzel is available online Gödel’s Proof - Hirzel’s translation: here PDF, though this is not recommended for reading in conjunction with this guide, since in Meltzer’s translation, in van Heijenoort’s translation, in the original German text, and in this guide the names for the various relations and functions are all the same, but they are different in Hirzel’s translation.) Confusingly, in some versions of the same translation, negation is indicated by horizontal bars over the negated entity; here we will use the ~ symbol for negation, which is the same as in the translations linked to above (note also that the original German text also uses overbars for negation). Note: you should be aware that there are some minor errors in Meltzer’s translation which are not in the original German text.
In this guide, a certain amount of basic knowledge of mathematical concepts is assumed. If your knowledge of these basic concepts is limited, then perhaps you should consider reading the simplified explanation of Gödel’s proof first.
Gödel’s proof can be broken down into the following principal parts:
This is Gödel’s introductory part of his paper (Part 1 of his paper) rather than the proof itself.
This is a method for assigning a unique number to every combination of symbols of the formal system - these numbers are sometimes called Gödel numbers. The proof is interested in certain relationships between certain combinations of symbols of the formal system, such as whether a certain string of symbols constitutes a proof of another string of symbols - in which case the first string is a proof, and the other is a valid formula of the system. The aim of the proof is to define relations between the Gödel numbers that precisely correspond to the relationships between the corresponding strings of symbols of the formal system - so that if the relationship between the symbol strings applies, then the corresponding relation between the corresponding Gödel numbers also holds. If this is done correctly, then the relations between the Gödel numbers mirror precisely the relationships between the corresponding symbol strings.
Gödel’s reason for introducing primitive recursion is that any number-theoretic relation that can be shown to be primitive recursive is a relation which can always be proved either correct or incorrect by a simple mechanical procedure. This property is used as a key part of the proof sketch for Gödel’s Proposition V.
Gödel defines 46 key relations/functions in the proof. This part deals with the first 23 of these.
This part deals with the remainder of the key relations/functions used in the proof
Using the previously defined relations, this proposition asserts that a certain relationship exists between every primitive recursive relation and a Gödel number that corresponds to that relation. The proposition includes the claim that propositions of the formal system can make logically valid propositions about propositions of the formal system itself, by way of Gödel numbering.
This is the assertion that there is a certain formula of the formal system P that the formal system cannot prove to be correct or incorrect, and yet it is a statement that must be either ‘true’ or ‘false’. This guide does not deal with this proposition nor any part of the paper past this point.
Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked (comments will be checked before appearing on this site). Difficulties in understanding the site content are usually best addressed by contacting me by e-mail. Note: you will be asked to provide an e-mail address - this will only be used to notify you of replies to your comments - it will never be used for any other purpose, will never be displayed and does not require verification. Comments are common to the entire website, so please indicate what section of the site you are commenting on.
If you cannot see any comments below, it may be that a plug-in on your browser is blocking Disqus comments from loading. Avast anti-virus in particular is known to do this, especially with Internet Explorer and Safari. See Disqus Browser plug-in/extension conflicts or Why isn’t the comment box loading?.
Please wait for comments to load …
There is now a new page on Lebesgue measure theory and how it is contradictory.
There is now a new page Halbach and Zhang’s Yablo without Gödel which demonstrates the illogical assumptions used by Halbach and Zhang.
It has come to my notice that, when asked about the demonstration of the flaw in his proof (see A Fundamental Flaw in an Incompleteness Proof by Peter Smith PDF), Smith refuses to engage in any logical discussion, and instead attempts to deflect attention away from any such discussion. If any other reader has tried to engage with Smith regarding my demonstration of the flaw, I would be interested to know what the outcome was.
I found that making, adding or deleting footnotes in the traditional manner proved to be a major pain. So I developed a different system for footnotes which makes inserting or changing footnotes a doddle. You can check it out at Easy Footnotes for Web Pages (Accessibility friendly).
I have now added a new section to my paper on Russell O’Connor’s claim of a computer verified incompleteness proof. This shows that the flaw in the proof arises from a reliance on definitions that include unacceptable assumptions - assumptions that are not actually checked by the computer code. See also the new page Representability.
There is now a new page on Chaitin’s Constant (Chaitin’s Omega), which demonstrates that Chaitin has failed to prove that it is actually algorithmically irreducible.
For convenience, there are now two pages on this site with links to various material relating to Gödel and the Incompleteness Theorem
– a page with general links:
– and a page relating specifically to the Gödel mind-machine debate:
All pages on this website are printer friendly, and will print the main content in a convenient format. Note that the margins are set by your browser print settings.
Comments on this site are welcome, please see the comment section.
Please note that this web site, like any other is a collection of various statements. Not all of this web site is intended to be factual. Some of it is personal opinion or interpretation.
If you prefer to ask me directly about the material on this site, please send me an e-mail with your query, and I will attempt to reply promptly.
Feedback about site design would also be appreciated so that I can improve the site.
Copyright © James R Meyer 2012 - 2017