Analyses of Incompleteness Proofs

Page last updated 03 Mar 2023

Several incompleteness proofs, like Gödel’s proof, claim to prove incompleteness of a formal language system and also claim that there is a formula of the formal system that is ‘true’ but unprovable in the formal system. These proofs all have obvious errors of logic, or make unfounded assumptions, or both. A brief synopsis of the types of errors in such proofs is given Errors in Incompleteness Proofs. Papers demonstrating the flaws in these proofs are now available, as follows:

1. PDF A Fundamental Flaw in an Incompleteness Proof by Peter Smith
2. PDF A Fundamental Flaw in Incompleteness Proofs by S. C. Kleene
3. PDF A Fundamental Flaw in Incompleteness Proofs by Gregory Chaitin
4. PDF A Fundamental Flaw in an Incompleteness Proof by George Boolos
5. PDF A Fundamental Flaw in an Incompleteness Proof by Stanisław Świerczkowski

There are also papers on the errors in three different proofs of incompleteness where the authors claim that the proof must be correct because it has been ‘checked’ by computer software:

6. PDF An Error in a Computer Verified Proof of Incompleteness by John Harrison
7. PDF An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor
8. PDF An Error in a Computer Verified Proof of Incompleteness by Natarajan Shankar

Brief details about the papers are given later below:

There is also a webpage on the errors in four different proofs of what is called the ‘Diagonal Lemma’ (see The Diagonal Lemma). The Diagonal Lemma uses an unfounded assumption to make it appear that a formal system can reference itself; once that is done, an incompleteness proof based on that is easily accomplished. There have also been claims of incompleteness proofs based on the so-called “MRDP theorem”, the proof of this by Yuri Matiyasevich is easily shown to be erroneous, relying on a conflation of levels of language that is a feature of most incompleteness proofs, see the page Hilbert’s tenth problem.

Similar assumptions are also used by Scott Aaronson, an Associate Professor in the Department of Electrical Engineering and Computer Science at the Massachusetts Institute of Technology, in two different “proofs” of incompleteness. The proofs are examined on the webpage The Halting Problem and Incompleteness Proofs.

I also now have a page to deal with incompleteness proofs that are so obviously flawed that it is not worth devoting a formal paper to them, you can see them at Yet Another Flawed Incompleteness Proof.

A Fundamental Flaw in an Incompleteness Proof by Peter Smith

The paper PDF A Fundamental Flaw in an Incompleteness Proof by Peter Smith deals with an incompleteness proof that is found in the Second Edition of a book by the convicted paedophile ex-professor Peter Smith, now available online: PDF “An Introduction to Gödel’s Theorems”  (Footnote: Peter Smith. An Introduction to Gödel’s Theorems. Cambridge University Press, 2006.
ISBN: 9780521857840 See An Introduction to Gödel’s Theorems: Details.) (For the paper that refers to the First Edition (2007) see PDF A Fundamental Flaw in an Incompleteness Proof by Peter Smith (v1) ). Smith makes the elementary error of the illegal substitution of a variable, as well as several erroneous assumptions (see Error of illegal substitution for a brief description of Smith’s principal error).

Note: Smith also used to have a PDF freely available on his website entitled Gödel Without (Too Many) Tears, I see that now he has taken it off his site, and he wants you to pay for it at Amazon. I have a copy of it, if you want it for educational purposes (the copyright specifically permits copying for educational use) I can send you a copy, just ask through my email or in a comment with your email address (I will then remove that address). It covers much of the same material as the book, but it skips over the crucial technical details, so it cannot really be recommended as a substitute for the book. The error in that article is essentially the same error as in the book, and it is dealt with on the page Peter Smith’s Gödel Without (Too Many) Tears - Or Not?. If you want to ask Peter Smith about the error in his proof, send him an email at peter [email protected]. If you get an interesting reply, please let me know.

Several authors have used the same basis as Smith for their proofs of incompleteness and the error can readily be demonstrated in the same way as the demonstration of the error in Peter Smith’s book. Among such proofs are:

1. “Gödel’s Incompleteness Theorems”, by Raymond M Smullyan (Footnote: Raymond M Smullyan. Gödel’s Incompleteness Theorems. Oxford University Press, 1992.
   ISBN: 0195046722 See Gödel’s Incompleteness Theorems: Details. )
2. “Recursion Theory for Metamathematics”, by Raymond M Smullyan (Footnote: Raymond M Smullyan. Recursion Theory for Metamathematics. Oxford University Press, 1993.
   ISBN: 9780195082326 See Recursion Theory for Metamathematics: Details. )
3. “Computability and Logic”, by George Boolos (Footnote: G Boolos, J Burges, and R Jeffrey. Computability and Logic. Cambridge University Press, fifth edition, 2007.
   ISBN: 9780521877527 See Computability and Logic: Details. )
4. “Gödel’s Theorem: An Incomplete Guide to its Use and Abuse”, by Torkel Franzén (Footnote: Torkel Franzén. Gödel’s Theorem: An Incomplete Guide to its Use and Abuse. A K Peters, 2005.
   ISBN: 1568812388 See Gödel’s Theorem: An Incomplete Guide to its Use and Abuse: Details. )
5. “Lecture Notes: Aspects of Incompleteness”, by Per Lindström (Footnote: Per Lindström. Lecture Notes: Aspects of Incompleteness. Springer-Verlag, 1997.
   ISBN: 3540632131. )
6. “Sentences Undecidable in Formalized Arithmetic”, by Andrej Mostowski (Footnote: Andrej Mostowski. Sentences Undecidable in Formalized Arithmetic. Greenwood Press, 1982.
   ISBN: 9780313231513 See Sentences undecidable in formalized arithmetic: Details. )

See also the two ‘computer verified’ proofs below by Harrison and O’Connor which also rely on the same error of substitution.

A Fundamental Flaw in Incompleteness Proofs by S. C. Kleene

The paper PDF A Fundamental Flaw in Incompleteness Proofs by S. C. Kleene deals with incompleteness proofs and related proofs that are to be found in two papers by Stephen Kleene. (Footnote: S. C. Kleene,
▪ General recursive functions of natural numbers. Mathematische Annalen, 112: pp 727-742, 1936, doi:10.1007/BF01565439. Not available free online, except at sci hub, see Current sci-hub active links or Latest Sci Hub Links and Download Research Papers and Scientific Articles for free.
▪ Recursive predicates and quantifiers.
Transactions of the American Mathematical Society, 53: pp 41-73, 1943. Available online PDF Recursive Predicates and Quantifiers.) Kleene’s errors are the error of using an unproven assumption, the error of language confusion, and the error of illegal substitution of variables (see Error of unproven assumption, Error of language confusion and Error of illegal substitution for a brief description of the errors).

An Error in Proofs of Incompleteness by Kleene and Rogers

There are also almost identical erroneous proofs of incompleteness in books by both Kleene and Rogers. The webpage Errors in incompleteness proofs by Kleene and Rogers describes the error which is common to a proof in Kleene’s book “Introduction to metamathematics” and a proof in Rogers’s book “Theory of Recursive Functions and Effective Computability”. Both authors make the egregious error of assuming that because they have been unable to discover a proof of a particular assertion, then the negation of that assertion must be true, and they use that fallacious assumption to generate a “proof ” of incompleteness.

A Fundamental Flaw in Incompleteness Proofs by Gregory Chaitin

The paper PDF A Fundamental Flaw in Incompleteness Proofs by Gregory Chaitin deals with incompleteness proofs that can be found in several papers by Gregory Chaitin. (Footnote: G. J. Chaitin,
▪ Computational Complexity And Gödel’s Incompleteness Theorem.
ACM SIGACT News, 9: pp 11-12, 1971. Not currently available online. ▪ Information-theoretic computational complexity.
IEEE Transactions on Information Theory, IT-20: pp 10-15, 1974. Not currently available online. ▪ Information-Theoretic Limitations of Formal Systems.
Journal of the ACM, 21: pp 403-424, 1974. Not currently available online. ▪ Algorithmic Information Theory.
IBM Journal of Research and Development, 21: pp 350-359, 1977. Not currently available online. ▪ Information Theoretic Incompleteness.
Applied Mathematics and Computation, 52: pp 83-101, 1992. Not currently available online.) Chaitin’s error is that he bases his proofs on an unproven assertion (see Error of unproven assumption for a brief description of the error).

A Fundamental Flaw in an Incompleteness Proof by George Boolos

The paper PDF A Fundamental Flaw in an Incompleteness Proof by George Boolos deals with an incompleteness proof in a paper by George Boolos. (Footnote: G Boolos. A New Proof of the Gödel’s Incompleteness Theorem.
Notices of the American Mathematical Society, 1989, v36 pp 388-390. ) Boolos’s error is that he bases his proofs on an unproven assertion (see Error of unproven assumption for a brief description of the error).

A Fundamental Flaw in an Incompleteness Proof by Stanisław Świerczkowski

The paper PDF A Fundamental Flaw in an Incompleteness Proof by Stanisław Świerczkowski deals with an incompleteness proof that is found in a paper by Stanisław Świerczkowski, called “Finite sets and Gödel’s incompleteness theorems”. (Footnote: Świerczkowski. Finite sets and Gödel’s incompleteness theorems.
Polska Akademia Nauk, Instytut Matematyczny, vol. 422, 2003. Available online Świerczkowski, Finite sets and Gödel’s incompleteness theorems.) Świerczkowski’s proof fails to make a clear distinction between when an expression is intended to represent an expression of the formal system, and when it is itself actually an expression of the formal system. This results in the bizarre claim that expressions of the formal system can refer to symbols of the meta-language, even though by definition the formal system can only refer to its own symbols. A logical analysis demonstrates that Świerczkowski’s ‘proof’ of this bizarre claim has no logical validity.

Lawrence Paulson has published some papers claiming a machine assisted proof of incompleteness that is based on Świerczkowski’s paper. (Footnote: L. Paulson,
▪ A Machine Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets.
The Review of Symbolic Logic (2013), 1–15. Available online PDF A Machine-Assisted Proof of Gödel’s Incompleteness Theorems.
▪ Gödel’s Incompleteness Theorems (Machine Code), Nov, 2013. Available online PDF Gödel’s Incompleteness Theorems, Machine Code. ) Paulson’s computer code is flawed in the same way as Świerczkowski’s proof.

An Error in a Computer Verified Proof of Incompleteness by John Harrison

The paper PDF An Error in a Computer Verified Proof of Incompleteness by John Harrison deals with an incompleteness proof that is found in a book by John Harrison, called “Handbook of Practical Logic and Automated Reasoning”. (Footnote: J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
ISBN: 9780521899574 (eBook format: ISBN: 9780511508653) Handbook of Practical Logic and Automated Reasoning: Details.) Harrison’s proof relies on the same illogical substitution of variables by values outside their allowable domain that is found in the proof by Peter Smith, see above.

An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor

The paper PDF An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor deals with an incompleteness proof that is found in an article by Russell O’Connor, called “Essential Incompleteness of Arithmetic Verified by Coq”. (Footnote: R. O’Connor,
Essential In completeness of Arithmetic Verified by Coq., 2005. Available online PDF Incompleteness of Arithmetic Verified by Coq.
Incompleteness & Completeness, 2009. Available online PDF Incompleteness & Completeness.) O’Connor’s proof relies on the same illogical substitution of variables by values outside their allowable domain that is found in the proof by Peter Smith, see above.

An Error in a Computer Verified Proof of Incompleteness by Natarajan Shankar

The paper PDF An Error in a Computer Verified Proof of Incompleteness by Natarajan Shankar deals with an incompleteness proof that is found in a book by Natarajan Shankar, called “Metamathematics, Machines, and Gödel’s proof.”  (Footnote: N. Shankar. Metamathematics, Machines, and Gödel’s Proof. Cambridge University Press, 1997.
ISBN: 9780521585330 Metamathematics, Machines, and Gödel’s Proof: Details.) The error in Shankar’s proof occurs when he uses a non-variable value where there should be a variable value.

Various other incompleteness proofs with errors

I have several other pages regarding errors in other incompleteness proofs:

The Diagonal Lemma as used in incompleteness proofs

Hilbert’s tenth problem and incompleteness

The Halting Problem and Incompleteness Proofs

World’s shortest explanation of Gödel’s Proof ?

Jean-Yves Girard on Incompleteness

Yet Another Flawed Incompleteness Proof