This page is keyboard accessible:
• Use Tab, Shift + Tab keys to traverse the main menu. To enter a sub-menu use the Right Arrow key. To leave a sub-menu use the Left Arrow or the Escape key.
• The Enter or the Space key opens the active menu item.
• To skip the menu and move to the main content, press Tab after the page loads to reveal a skip button.
• To get back to the top of the page anytime, press the Home key.
• For more information, click here: Accessibility   Close this tip.

Note: Full functionality of this web page requires JavaScript to be enabled in your browser.

A Step by Step Guide to Gödel’s Incompleteness Proof:





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.


Note that (provided you have JavaScript enabled) clicking on (hideshow) will reveal further details, while clicking again will hide it. Also, clicking on (hideshow Gödel’s) will reveal relevant parts of Gödel’s text (shown in green), while clicking again will hide it. Please note that older browsers may not display some symbols correctly.


(like this)


(like this)


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.



Parts of the Proof

Gödel’s proof can be broken down into the following principal parts:

Part 1: Gödel’s introduction

This is Gödel’s introductory part of his paper (Part 1 of his paper) rather than the proof itself.

Part 2: The definition of the formal system

Gödel’s paper defines in precise detail a formal system; the goal of Gödel’s proof is to prove that this formal system is incomplete.


Part 3: The axioms and rules of inference

Here Gödel defines the axioms and the rules of inference of the formal system.


Part 4: The Gödel numbering system

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.


Part 5: The definition of primitive recursion

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.


Part 6: Gödel’s definitions of functions and relations 1-23

Gödel defines 46 key relations/functions in the proof. This part deals with the first 23 of these.


Part 7: Gödel’s definitions of functions and relations 24-46

This part deals with the remainder of the key relations/functions used in the proof


Part 8: Gödel’s Proposition V

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.


Gödel’s Proposition VI

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 …  


The Lighter Side



There’s something about Gödel by Francesco Berto

There is a new addition to the page Yet another flawed incompleteness proof, where Berto’s proof of incompleteness in his book There’s something about Gödel comes under scrutiny.



Easy Footnotes

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).



O’Connor’s “computer checked” proof

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.



New page on Chaitin’s Constant

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.



Updated: Diagonal Lemma

Flawed proofs of the Diagonal Lemma by Panu Raatikainen and Vann McGee have been added to the Diagonal Lemma web page.

Previous Blog Posts  


16th Mar 2015 Bishops Dancing with Pixies?


23rd Feb 2015 Artificial Intelligence


31 Mar 2015 Cranks and Crackpots


30 Apr 2015 The Chinese Room




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:

Gödel Links


– and a page relating specifically to the Gödel mind-machine debate:

Gödel, Minds, and Machines


Printer Friendly


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.

Note: for some browsers JavaScript must be enabled for this to operate correctly.




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 - 2016