Logic and
Load the menuLoad the menu

Copyright   James R Meyer    2012 - 2024 https://www.jamesrmeyer.com

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





Page last updated 28 Dec 2022


Now printer friendly: this guide has now been set up for easy printing so that readers can also access the information in paper format.


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). 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 PDF Gödel’s Proof by E Nagel and J Newman New York University Press, revised edition, 2001.
ISBN: 0814758169.)
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 to 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 gleaming polished 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. (Footnote: This translation is recommended as it has clickable cross-reference links, but there are other English translations available. A translation by Meltzer was freely available online for many years but it now seems that many sites want you to pay for it, and hide it behind a pay wall, but you may find it online at PDF AltExploit - Meltzer’s translation and PDF Minnesota State University - Meltzer’s translation. Note that there are some minor errors in Meltzer’s translation which are not in the original German text. 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. There are arguments as to which English translation is the ‘best’ and most faithful to the German original (which you can see at PDF Gödel’s original proof in German), 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 at PDF Hirzel’s translation of Gödel’s Incompleteness paper; however, it 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; the symbols ¬ or ~ are also used in other translations (note also that the PDF original German text also uses overbars for negation).


Note that (provided you have JavaScript enabled) clicking on () will reveal further details, while clicking again will hide it. Also, clicking on () will reveal relevant parts of Gödel’s text (shown in green), while clicking again will hide it.


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






Interested in supporting this site?

You can help by sharing the site with others. You can also donate at Go Get Funding: Logic and Language where there are full details.



As site owner I reserve the right to keep my comments sections as I deem appropriate. I do not use that right to unfairly censor valid criticism. My reasons for deleting or editing comments do not include deleting a comment because it disagrees with what is on my website. Reasons for exclusion include:
Frivolous, irrelevant comments.
Comments devoid of logical basis.
Derogatory comments.
Long-winded comments.
Comments with excessive number of different points.
Questions about matters that do not relate to the page they post on. Such posts are not comments.
Comments with a substantial amount of mathematical terms not properly formatted will not be published unless a file (such as doc, tex, pdf) is simultaneously emailed to me, and where the mathematical terms are correctly formatted.

Reasons for deleting comments of certain users:
Bulk posting of comments in a short space of time, often on several different pages, and which are not simply part of an ongoing discussion. Multiple anonymous user names for one person.
Users, who, when shown their point is wrong, immediately claim that they just wrote it incorrectly and rewrite it again - still erroneously, or else attack something else on my site - erroneously. After the first few instances, further posts are deleted.
Users who make persistent erroneous attacks in a scatter-gun attempt to try to find some error in what I write on this site. After the first few instances, further posts are deleted.

Difficulties in understanding the site content are usually best addressed by contacting me by e-mail.


Based on HashOver Comment System by Jacob Barkdull

Copyright   James R Meyer   2012 - 2024