Note: Full functionality of this website requires JavaScript to be enabled in your browser.
Analyses of Incompleteness Proofs
Page last updated 09 Nov 2022
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:
- A Fundamental Flaw in an Incompleteness Proof by Peter Smith
- A Fundamental Flaw in Incompleteness Proofs by S. C. Kleene
- A Fundamental Flaw in Incompleteness Proofs by Gregory Chaitin
- A Fundamental Flaw in an Incompleteness Proof by George Boolos
- 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:
- An Error in a Computer Verified Proof of Incompleteness by John Harrison
- An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor
- 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 web page 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 shown to be erroneous on this 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 web-page 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 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 Peter Smith, now ava\ilable online: “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 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 smith@me.com. 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:
- “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. ) - “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. ) - “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. ) - “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. ) - “Lecture Notes: Aspects of Incompleteness”, by Per Lindström (Footnote:
Per Lindström. Lecture Notes: Aspects of Incompleteness. Springer-Verlag, 1997.
ISBN: 3540632131. ) - “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 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, https://sci-hub.se, see also Current sci-hub active links and Download Research Papers and Scientific Articles for free.) (Footnote:
S. C. Kleene. Recursive predicates and quantifiers.
Transactions of the American Mathematical Society, 53: pp 41-73, 1943. Available online 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).
A Fundamental Flaw in Incompleteness Proofs by Gregory Chaitin
The paper 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.)
(Footnote:
G. J. Chaitin. Information-theoretic computational complexity.
IEEE Transactions on Information Theory, IT-20: pp 10-15, 1974. Not currently available online.)
(Footnote:
G. J. Chaitin. Information-Theoretic Limitations of Formal Systems.
Journal of the ACM, 21: pp 403-424, 1974. Not currently available online.)
(Footnote:
G. J. Chaitin. Algorithmic Information Theory.
IBM Journal of Research and Development, 21: pp 350-359, 1977. Not currently available online.) (Footnote:
G. J. Chaitin. 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 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 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 A Machine-Assisted Proof of Gödel’s Incompleteness Theorems.)
(Footnote:
L. Paulson. Gödel’s Incompleteness Theorems (Machine Code), Nov, 2013. Available online 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 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 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 Incompleteness of Arithmetic Verified by Coq.) (Footnote: R. O’Connor. Incompleteness & Completeness, 2009. Available online 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 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.
Footnotes:
Interested in supporting this site?
You can help by sharing the site with others. You can also donate at _{} 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.