Dr. Barendregt occasionally gets emails from people claiming to have found a flaw in Gödel’s incompleteness theorem. Sometimes Dr. Barendregt forwards these emails to me. Since I have created a complete computered verified formal proof of the first incompleteness theorem, I have a pretty good understanding of how the proof works.
One such submission was made by James R. Meyer. He has publically published his work on his website, outside the usual academic publishing routes. There is nothing wrong with this, especially given that he is not an academic. Given his choice, it seems reasonable to for people like me to respond by publishing reviews of his work on the web as well. The following is my review of one of his papers. I have passed a draft copy of this review to Mr. Meyer before publishing it here.
The paper “The Fundamental Flaw in Gödel’s Incompleteness Theorem” (V 1-210608, 2007) claims to demonstrate an error in Gödel’s first incompleteness theorem. However, the reasoning is based on a misunderstanding of the theorem and logical axioms. Essentially, the author ends up working in a system belonging to a well-known class of inconsistent logical systems. This is why his deductions contradict accepted results.
This section gives two attempts at stating the first incompleteness theorem. The author’s first characterization claims the Gödel sentence is unprovable but true. His second characterization claims the Gödel sentence is unprovable in the inner logical system but is provable in meta-logical system. Neither of these two statements properly characterize Gödel’s theorem.
A modern version of Gödel’s theorem states that for any sufficiently powerful recursive set of axioms that is (ω-)consistent, there is a (Π1) sentence that is unprovable, and whose negation is also unprovable. Gödel’s original proof requires ω-consistency, while Rosser’s improvement only requires consistency.
One can verify that my version is the correct statement of Gödel’s theorem by reading Hirzel’s translation of Theorem VI.
Theorem VI: For every ω-consistent primitive recursive class κ of formulae there is a primitive recursive class-sign r such that neither forall(v, r) nor not(forall(v, r)) belongs to Conseq(κ) (where v is the free variable of r).
At this point the author attempts to counter claims that the Gödel statement isn’t proven or isn’t true. The reality is that the Gödel sentence is definitely not proven and may not be true. He attempts to counter this view in a footnote:
There are even those who reject any notion that the ‘unprovable’ formula given by Gödel’s theorem can in any way be considered to be true or provable. Among such curious notions is that Gödel’s proof only asserts a conditional: “If the formal system is consistent, then there is a formula of the formal system, which is not provable by the formal system, but it is true.” Such arguments ignore the obvious fact that every proved expression is dependent upon the assumptions used in its generation; such conditionals could be pedantically applied to the result of every proof, and there is no obvious reason why this conditional should be treated any differently.
Indeed the author is right that we can say the condition “If the formal system is consistent, then the Gödel sentence is true”. He is also right that there is no obvious reason why we should pedantically apply this condition. However, the author fails to realize that there is an extremely important, non-obvious reason that we pedantically include this conditional.
It would seem to be quite natural to assume that one is working in a consistent formal system. Why not go further and take the consistency of the system as an axiom? The first problem one encounters is trying to create an axiom system that includes an axiom stating that the system is consistent because the statement must refer to the system that contains the statement we are trying to write. One cannot simply add the axiom “T is consistent” to the system T, because the resulting system T′:=T+“T is consistent” is different from T. Thus T′ fails to assert its own consistency. Fortunately, using Gödel’s techniques, this problem is actually surmountable, and we can create an axiom system that contains an axiom that asserts its own consistency. (Ironically, if the author believes in the consequences of his claim, then he isn’t allowed to create the axiom that says his own system is consistent that his own reasoning relies on.)
Suppose T is such a recursive system such that “T is consistent” is a member of T and contains Peano arithmetic. Then we can apply Gödel’s second incompleteness theorem to construct a proof of False in T. Any system containting its consistency as an axiom (or as a consequence) is inconsistent.
Mathematicians find themselves in the curious situation that, while they believe the system the are working in is consistent, they are unable to apply this belief to their work. They must always work in a system that is agnostic about its own consistency.
This is why we pedantically apply the conditional to such statements. The condition cannot be an axiom of whatever deduction system we are using. The reason we add the conditional the this statement and not other typical mathematical statements, is that this deduction makes essential use of the assumption, where as most mathematical deductions do not.
The author then discusses the paradox that his incorrect characterizations of Gödel’s theorem leads to. However, a correct version of the theorem, or a version that properly uses the consistency conditional, has no such paradox.
I will also note that, although Gödel’s proof may use proof by contradiction at some point, as the author claims, this use is not essential. Indeed, I have created a constructive proof of the incompleteness theorem.
The author claims that Gödel has made a logical flaw in proposition V, which he address in detail in section (10).
I have looked through these sections, but have not scoured them for errors. These sections do not appear to make any controversial claims, and essential errors have been found in the other sections. Therefore, a detailed review of these sections is unnecessary.
The author makes an error in proving his version of Gödel’s Theorem. It is important to note that he is attempting to prove his erroneous version of the incompleteness theorem. If we ignore the incorrect use of logical notation through the proof, we can pinpoint his error in line 9.1.18 where at the end he says,
This means that the relation ¬Bew{Sb[q, 17, Z(q)]} holds. Since that is the case, then there cannot be a formal proof of the formal formula that corresponds to Sb[q, 17, Z(q)].
We cannot conclude that there is no formal proof of Sb[q, 17, Z(q)] without using an assumption that the system is consistent. As I discussed above, we cannot use the assumption that our system is consistent in logical arguments.
The author claims that Gödel confuses ‘number-theoretic relations’ as both a meta-language and sub-language. Although this is a confusing part of Gödel’s proof, the distinction between ‘number-theoretic relations’ as part of the meta-language and sub-language can be teased apart. I have done so in my formal proof where the inductive type defining the primitive recursive function corresponds to a formal sub-language. A function called evalPrimRec converts these formal structures into actual functions in the meta-language. The evalPrimRec function is essentially an interpreter for the mini-programing language of primitive recursive functions.
There is no problem assigning variables in the meta-language to the correspond to variables in the sub-language because it is not necessary for the “names” of the variables to match. One simply matches the nth variable applied in the meta-language with the nth variable applied in the sub-language, choosing whatever names are convenient to use in the meta-language. In fact, in my definition of primitive recursive functions combinators are used so named variables do not even appear in the sub-language.
This same distinction can be done with ‘number-theoretic relations’ as well as primitive recursive functions. An interpreter function converts formal ‘number-theoretic’ relations as a sub-language into an actual relation in the meta-language, matching the nth variable applied in the meta-language (using whatever names one wishes) with the nth variable applied in the sub-language.
I do sympathize with the author though. Discussion about variables have been very subtly muddled in presentations of Gödel’s theorem that I have read. However, these issues can be dealt with properly.
This is not an essential flaw with Gödel’s argument and all the problems discussed in this chapter disappear. For example, there is no longer any problem with the notion of a ‘number-theoretic relation’ R being true or false at a given value. Saying “R(5) is true” simply means that eval(R) holds at 5.
The author claims Gödel’s proof superficially appears to state that that proof itself could not be expressed in a
formal language, and in so doing, appears to absolve itself from the rigour required of formal
languages.
and
No-one to date has given a satisfactory explanation as to why there cannot be a logically
coherent formalization of Gödel’s argument.
However, there have been at least three computer formalizations of Gödel’s first incompleteness theorem. I have created one of them. Each of the formalizations give a complete, logically coherent formal proof that is similar in character to Gödel’s original argument but in a formal language.
There are three essential errors the author makes. The first error is using an incorrect statement of Gödel’s theorem. The second error is working in a meta-system that implicitly assumes its own consistency. Although non-obvious, it is well-know to mathematicians that such a system is inconsistent. Thus it is not surprising that the author is able to derive results that contradict Gödel’s results.
The third error is his attempt to find a flaw in Gödel’s Proposition V. As the author notes, Gödel omits the details of this deduction, leaving it for the reader to fill in. Unfortunately, the author has not correctly filled in the details himself. Perhaps Gödel (and other writers) could have been more clear about the distinction between the sub-language of ‘number-theoretic relations’ and its interpretion as a relation in the meta-language by explicitly writing out the uses of the ‘evaluation’ function converting the sub-language into the meta-language. It is indeed tricky to get this part right. I refer the reader to any one of the formal computer-verified proofs to see the details about how this can be done properly.
The paper is full of other less significant errors. The author incorrectly uses the logical implication symbol (⇒). The author always implicitly assumes that the inner axiom system in question is sound (which is a separate issue from consistency). Also, most of the time he assumes that logic of the inner system is identical to the logic of the meta-system. All these minor errors and hidden assumptions make the thinking behind this work difficult to decipher. However, I believe I have managed to understand the authors intent, and uncovered the essential errors in his reasoning.
Mr. Meyer has a response to my review.
See also James R Meyer vs Kurt Gödel.