• 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 get back to the top of the page anytime, press the Home key.

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

# Analyses of Incompleteness Proofs

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:

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:

Brief details about the papers are given 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.

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 web page to them, you can see them at Yet Another Flawed Incompleteness Proof.

## A Fundamental Flaw in an Incompleteness Proof by Peter Smith PDF

This paper deals with an incompleteness proof that is found in the Second Edition of a book by Peter Smith, called “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: here for a brief description of Smith’s principal error).

Note: Smith has a downloadable PDF on his website Logic Matters: Gödel Without (Too Many) Tears which covers much of the same material as the book, but it skips over the crucial technical details, so it cannot 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 Gödel Without 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:

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 Available online Aspects of Incompleteness: here.)
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 PDF

This paper 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. Not available free online, except at sci hub, http://sci-hub.tw/, see also 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: here PDF.)
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: here, Error of language confusion: here and Error of illegal substitution: here for a brief description of the errors).

## A Fundamental Flaw in Incompleteness Proofs by Gregory Chaitin PDF

This paper 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: here for a brief description of the error).

## A Fundamental Flaw in an Incompleteness Proof by George Boolos PDF

This paper 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: here for a brief description of the error).

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

This paper 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: here PDF.)
Ś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: here PDF.)
(Footnote: L. Paulson. Gödel’s Incompleteness Theorems (Machine Code), Nov, 2013. Available online Gödel’s Incompleteness Theorems, Machine Code: here PDF.) 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 PDF

This paper 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 PDF

This paper 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: here.) (Footnote: R. O’Connor. Incompleteness & Completeness, 2009. Available online Incompleteness & Completeness: here PDF.) 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 PDF

This paper 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:

Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked. 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 - any address will do, it does not require verification. Your e-mail will only be used to notify you of replies to your comments - it will never be used for any other purpose and will not be displayed. If you cannot see any comments below, see Why isn’t the comment box loading?.

## NEWS

### Lebesgue Measure

There is now a new page on a contradiction in Lebesgue measure theory.

### Illogical Assumptions

There is now a new page Halbach and Zhang’s Yablo without Gödel which analyzes the illogical assumptions used by Halbach and Zhang.

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

### Previous Blog Posts

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:

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

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.