Logic and Language

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

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

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

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.)  (Footnote: S. C. Kleene. 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).

## 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.)
(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 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.)
(Footnote: L. Paulson. 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.)  (Footnote: R. O’Connor. 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.

## Errors in incompleteness proofs by Kleene and Rogers

The page Errors in incompleteness proofs by Kleene and Rogers describes an error common to incompleteness proofs in Kleene’s book “Introduction to metamathematics ” and in Rogers’s book “Theory of Recursive Functions and Effective Computability ”.

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

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:
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 - 2023
https://www.jamesrmeyer.com