Analysis 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 here. Papers demonstrating the flaws in these proofs are now available, as follows:

1. A Fundamental Flaw in an Incompleteness Proof By Peter Smith (PDF)
2. A Fundamental Flaw in Incompleteness Proofs By S. C. Kleene (PDF)
3. A Fundamental Flaw in Incompleteness Proofs By Gregory Chaitin (PDF)
4. A Fundamental Flaw in an Incompleteness Proof By George Boolos (PDF)

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:

5. An Error in a Computer Verified Proof of Incompleteness by John Harrison (PDF)
6. An Error in a Computer Verified Proof of Incompleteness by Russell O'Connor (PDF)
7. An Error In A Computer Verified Proof of Incompleteness By Natarajan Shankar (PDF)

Brief details about the papers are given below:

Paper 1: A Fundamental Flaw in an Incompleteness Proof by Peter Smith (PDF)

This paper deals with an incompleteness proof that is found in a recently published book by Peter Smith, called "An Introduction to Gödel's Theorems" (for full details, see [1]). Smith makes the elementary error of the illegal substitution of a variable, as well as several erroneous assumptions (see here for a brief description of Smith's principal error). Several authors have using 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 [2]
2. "Recursion Theory for Metamathematics", by Raymond M Smullyan [3]
3. "Computability and Logic", by George Boolos [4]
4. "Gödel's Theorem: An Incomplete Guide to its Use and Abuse", by Torkel Franzén [5]
5. "Lecture Notes: Aspects of Incompleteness", by Per Lindström [6]
6. "Sentences Undecidable in Formalized Arithmetic", by Andrej Mostowski [7]
7. "Gödel's Proof", by E Nagel and J Newman [8]

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

Paper 2: 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 (see [9], [10]). 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 here, here and here for a brief description of the errors).

Paper 3: 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 (see [11], [12], [13], [14], [15] ). Chaitin's error is that he bases his proofs on an unproven assertion (see here for a brief description of the error).

Paper 4: A Fundamental Flaw in an Incompleteness Proof by George Boolos (PDF)

This paper deals with an incompleteness proof in a paper by George Boolos (see [16]). Boolos's error is that he bases his proofs on an unproven assertion (see here for a brief description of the error).

Paper 5: 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 Harrision, called "Handbook of Practical Logic and Automated Reasoning" (for full details, see [17]). Harrison's proof relies on the same illogical substitution of varaibles by values outside their allowable domain that is found in the proof by Peter Smith, see above.

Paper 6: 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" (for full details, see [18] and [19]). O'Connor's proof relies on the same illogical substitution of varaibles by values outside their allowable domain that is found in the proof by Peter Smith, see above.

Paper 7: 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." (for full details, see [20]). The error in Shankar's proof occurs when he uses a non-variable value where there should be a variable value.