A Step by Step Guide to
Gödel’s Incompleteness Proof:
Page last updated 28 Dec 2022
It 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 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 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:
The above 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/
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/
Part 7: Gödel’s definitions of functions and relations 24-46
This part deals with the remainder of the key relations/
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.
Rationale: Every logical argument must be defined in some language, and every language has limitations. Attempting to construct a logical argument while ignoring how the limitations of language might affect that argument is a bizarre approach. The correct acknowledgment of the interactions of logic and language explains almost all of the paradoxes, and resolves almost all of the contradictions, conundrums, and contentious issues in modern philosophy and mathematics.
Please see the menu for numerous articles of interest. Please leave a comment or send an email if you are interested in the material on this site.
Interested in supporting this site?
You can help by sharing the site with others. You can also donate at where there are full details.