# A review of Gödel’s flaw by Russell O’Connor

Page last updated 29 Sep 2020

Russell O’Connor has published a Review by O’Connor of my paper demonstrating the flaw in Gödel’s proof. His entire ‘review’ purports to refer to errors in the paper. However, at no point in his review does O’Connor specify an erroneous step in the demonstration of the flaw in Gödel’s proof, nor does he give any information that might enable the reader to find such a step in the paper.

After publishing his review, O’Connor later admitted to me that he did not know whether had Gödel made a mistake in his proof, and that he had not actually *‘read his original (translated) proof in careful detail’*. It’s hard to know whether to be amused or saddened by the fact that a man who has studied logic at university level thought that he was qualified to review a paper on Gödel’s original proof when by his own admission, he wasn’t familiar with the details of that proof. (And this is not an isolated case; there must be something very wrong with the teaching of logic when its graduates find it so difficult to apply logic to everyday situations).

Interestingly, O’Connor writes in a later blog post James R Meyer vs Kurt Gödel that a certain contributor in a web forum *“probably does a better job arguing the case than I ever could”*, which seems to be an admission that perhaps he wasn’t the most suitable person to review my paper. Unfortunately, O’Connor doesn’t give any details of this argument, instead expecting the reader to plough through a web forum which has 173 posts to try to discover the alleged errors in the logic of my argument. See also the section below, Another reference to my paper by O’Connor.

O’Connor has written and published what he claims is a version of Gödel’s proof completely written in a formal language that has been checked by a computer program. His review is based on the notion that one should accept his argument that - because my version of Gödel’s proof must be correct, then your demonstration of a flaw in Gödel’s original proof must be incorrect. * Update: O’Connor’s proof has been examined and a fundamental error has been discovered in it. The details can be seen at Analysis of O’Connor proof*.

O’Connor’s original review is written in green. My comments are written in black italic. I have included his web references. Note that the references to section numbers are to version 1 of the paper (210608).

## Overview

The paper, PDF Paper, previous v1: The Fundamental Flaw in Gödel’s Proof of his Incompleteness Theorem (V 1-210608, 2007) (Note: The current version is The Fundamental Flaw in Gödel’s Proof of his Incompleteness Theorem but the argument remains the same) 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.

MY COMMENT

O’Connor claims that I misunderstand Gödel’s proof. The fact is that I have created a walk-through guide to Gödel’s original incompleteness proof, and which is intended to be read alongside the paper. If you think that O’Connor might be correct in claiming that I don’t understand Gödel’s proof, I suggest that you take a look at it; it may help you to decide whether it is reasonable to suggest that I do not understand the proof. When I decided to make that guide, I did an intensive search to see if there was anything similar already published anywhere, but I found no detailed guide at all - so I constructed my guide from scratch - which I would claim is hardly indicative of someone who does not understand Gödel’s proof.

## Errors in (4) Preface

MY COMMENT

I had thought of adding a note stating that my preface was not to be taken as part of the main argument of my paper, but decided that it was so obvious that it would be pedantic to do so. Obviously I was wrong. What O’Connor terms ‘errors’ in my preface have no bearing on the main argument that I present in my paper. I have since revised my paper to include such a note.

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 (omega-)consistent, there is a (Pi1) sentence that is unprovable, and whose negation is also unprovable. Gödel’s original proof requires omega-consistency, while Rosser’s improvement only require 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 omega-consistent primitive recursive class kappa of formulae there is a primitive recursive class-sign r such that neither forall(v, r) nor not(forall(v, r)) belongs to Conseq(kappa) (where v is the free variable of r).

MY COMMENT

All the above is irrelevant. My comments about the interpretation of Gödel’s proof which were never intended to be taken as part of the actual demonstration of the flaw in the Gödel’s argument.

It does however show the limitations of O’Connor’s understanding. In the above he states on the one hand that Gödel’s theorem is the generalized version that he first states (which is similar to Gödel’s Proposition IX), and on the other hand he states that Gödel’s theorem is the theorem for a particular formal system and which is Gödel’s Theorem VI. The generalized version claims incompleteness for all formal systems that satisfy certain conditions, whereas the other claims incompleteness only for the defined formal system.

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.

MY COMMENT

Well, here O’Connor differs from Gödel’s own statements in his paper on this issue, which was that the Gödel sentence is proven and is true. And since I actually refer to this in my preface, one has to wonder how O’Connor can come to this conclusion. I stated in my preface:

Gödel’s paper itself refers to the statement as ‘decidable’ – “The proposition which is undecidable in the [formal] system turns out to be decided by meta-mathematical considerations.”

Furthermore, it is quite clear from Gödel’s footnote 48a that his stance is that the undecidable propositions of a formal system are not absolutely undecidable – and hence Gödel’s position is that they must be true or false: “It can be shown, that is, that the undecidable propositions here presented always become decidable by…”).

It is also interesting that O’Connor states that the Gödel sentence is definitely not proven; he appears to be quite confused about this. He earlier sent me an e-mail which included the following:

“I have not proved that the constructed formula is “true”… I have no doubt that this could be formalized, but I have not done so.”

Shortly after that he sent me another e-mail:

“I take back [the above] sentence. Upon reflection, I see that things are more subtle than I had thought. In general it is not possible to prove the constructed formula. The formula (of course) depends on the theory T under consideration … In the specific case where T is taken to be PA, then the generated formula will be provable… . (although I have not developed the proof)…”

So here he appears to be stating that the Gödel sentence, in his ‘version’ of Gödel’s proof, could be provable under certain conditions - O’Connor appears to be very confused. By the way, a general overview of the claim that the ‘unprovable’ statement cannot be said to be ‘true’ or proven is given at True but unprovable.

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.

MY COMMENT

O’Connor conveniently leaves out the remainder of the footnote which answers his argument below, and which is: In any case, the acceptance of Gödel’s proof must also include the assumption that Gödel’s proof language itself is consistent. Since Gödel’s proof is asserted to apply for any formal system that includes arithmetic, if it is assumed that there exists at least one consistent formal system that includes arithmetic, one can dispense with the above conditional. It would be completely absurd to assume that Gödel’s proof language (which itself includes arithmetic) itself is consistent, while at the same time asserting that one cannot assume that there exists at least one consistent formal system that includes arithmetic.

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.

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 containing it’s consistency as an axiom (or as a consequence) is inconsistent.

Mathematicians find themselves in the curious situation that, while they believe the system they 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 to this statement and not other typical mathematical statements, is that this deduction makes essential use of the assumption, whereas most mathematical deductions do not.

MY COMMENT

This is simply wrong. Of course you can make the assumption that the formal system is consistent – and thereby make it an axiomatic statement – in the meta-language. O’Connor appears to be confusing the assumption of consistency within a language and from outside a language.

The author then discusses the paradox that his incorrect characterizations of Gödel’s theorem leads to. However the corrected version, 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.

MY COMMENT

Again, O’Connor dismisses my comments regarding Gödel’s original paper, which is the paper that my own paper refers to, on the basis of irrelevant references to his own paper. And as already noted, none of my preface was ever intended to be read as part of my main argument.

The author claims that Gödel has made a logical flaw in proposition V, which he address in detail in section (10).

## Sections (5) through (8)

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.

MY COMMENT

This is ludicrous. Sections 5 through 8 contain the main material of the paper, which includes the detailed demonstration of the origin of the flaw in Gödel’s original paper. Why O’Connor should consider that a detailed review of that part of my paper - which contains the main argument - is unnecessary is quite unfathomable.

## Errors in (9) A Simplified Version of Gödel’s Theorem

The author makes an error in proving his version of Gödel’s Theorem. It is important to note that he attempting to prove his erroneous version of the incompleteness theorem rather than Gödel’s version. 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*)].

Again, we cannot conclude that there is no formal proof of Sb[q, 17, Z(q)] without assuming that our system is consistent. As I discussed above, we cannot use the assumption that our system is consistent in logical arguments.

MY COMMENT

This is patent nonsense. O’Connor states that one cannot assume that a system is consistent in logical arguments.

The gross stupidity of this assertion is obvious; for example, one can observe that Gödel also had to assume the consistency of his proof system (as well as the formal system) in order to obtain his result. O’Connor fails to see that his claim that one cannot assume the consistency of a proof system also asserts that Gödel’s result is invalid!

Of course one can make the assumption that a system is consistent, provided one makes it evident that one is making such assumptions. Clearly the result of the argument is dependent on those assumptions. And in any case every mathematical proof assumes the consistency of the system used in the proof. And in fact I do specifically state (in my 9.1.4) that I am “assuming consistency of the formal system.” So when O’Connor says I cannot assume that my system is consistent, he is wrong – I did do it. I can only presume that what he means is that the assumption of consistency leads to an error in the subsequent argument – but he gives no indication of how any such error might arise.

Quite obviously, my simplified version could simply be rewritten as, “If the formal system is consistent, then…”, and it would still give the essence of Gödel’s result. This would bypass O’Connor’s pedantic remarks which do not indicate an error at all – only that my simplified version is not written in the way he thinks it should be written.

In any case, my simplified version of Gödel’s proof is not actually necessary in my demonstration of the flaw in Gödel’s proof, as I note at the start of Section 10 of my paper - so that even if there was an error in my simplified proof, that would have no bearing at all on my demonstration of the flaw in Gödel’s proof.

O’Connor also mentions ‘incorrect use of logical notation’ without giving any idea of what he means by this.

## Errors in (10) The Inherent Flaw in Gödel’s Theorem

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 (Essential Incompleteness of Arithmetic Verified by Coq) 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-programming language of primitive recursive functions.

MY COMMENT

O’Connor simply avoids any detailed reference to my paper at all, and simply introduces irrelevant references to terms from his own paper such as “evalPrimRec”, a term which does not occur either in my paper or Gödel’s paper.

There is no problem assigning variables in the meta-language to correspond to variables in the sub-language because it is not necessary for the “names” of the variables to match. One simply matches the `n`^{th} variable applied in the meta-language with the `n`^{th} 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.

MY COMMENT

Again, O’Connor simply avoids any detailed reference to my paper at all. I have no idea of what part of my Section 10 he might be referring to. I never stated that the names of the variables have to match; in fact there is no mention of ‘name’ or ‘names’ in my entire paper.

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 `n`^{th} variable applied in the meta-language (using whatever names one wishes) with the `n`^{th} variable applied in the sub-language.

MY COMMENT

Again, O’Connor simply avoids any detailed reference to my paper at all. Again, he gives no idea of what part of my Section 10 he might be referring to. Again, he introduces irrelevant references to terms from his own paper such as “interpreter function”, a term which does not occur either in my paper or Gödel’s paper.

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.

MY COMMENT

Yet again, O’Connor simply avoids any detailed reference to my paper at all, and simply introduces irrelevant references to terms from his own paper such as “(eval R)”, a term which does not occur either in my paper or Gödel’s paper.

One may wonder what he intends to mean by “I do sympathize with the author”. Perhaps he intends to imply that he believes that I am so sadly mistaken that I am to be pitied. But while O’Connor blithely states that ‘… all the problems in this chapter disappear’, one cannot escape the fact that O’Connor continues to avoid actually demonstrating how I might be mistaken, sadly or not.

## Response to (11) Summary

The author claims “Gödel’s proof superficially appears to state that the 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 (Essential Incompleteness of Arithmetic Verified by Coq). Each of the formalizations give a complete, logically coherent formalization of Gödel’s argument in a formal language.

MY COMMENT

Since O’Connor has refused to deal with any detail of my main argument, and refused to actually show where my main argument is wrong, it is pointless commenting on this. The three ‘computer formalizations’ of “Gödel’s incompleteness theorem” that O’Connor refers to have each been examined and fundamental errors have been discovered in each of them, so that O’Connor’s claim that there is a coherent formalization of Gödel’s argument in a formal language is incorrect. The details can be seen at

*PDF An Error in a Computer Verified Proof of Incompleteness by John Harrison**PDF An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor**PDF An Error in a Computer Verified Proof of Incompleteness by Natarajan Shankar*

## Conclusion

There are three essential errors the author makes.

The first error is using an incorrect statement of Gödel’s theorem.

MY COMMENT

Even if it was true that I used an ‘incorrect’ statement of Gödel’s theorem, it would be utterly irrelevant. This is so since my demonstration of the flaw is a demonstration of a flaw in Gödel’s Proposition V, a proposition upon which Gödel’s Proposition VI depends (Proposition VI being Gödel’s incompleteness proposition for the defined formal system). For this reason, I have no need whatsoever to state what is commonly called “Gödel’s incompleteness theorem”, or refer to the statement of the theorem in order to demonstrate the flaw in Gödel’s proof.

The only sections where there are statements that might be deemed a statement of Gödel’s theorem such as O’Connor might be referring to are in my preface and in my simplified version of Gödel’s proof. These sections can be removed completely from my paper without affecting my demonstration of the flaw in Gödel’s proof.

The second error is working in a meta-system that implicitly assumes its own consistency. Although non-obvious, it has been shown 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.

MY COMMENT

This is blatant nonsense. Every mathematician/

My conclusion is that O’Connor is desperately attempting to provide some plausibility for his dismissal of my paper, since he was quite unable to find any flaw within my argument.

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 interpretation 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. * Update: O’Connor’s proof has been examined and a fundamental error has been discovered in it. The details can be seen at* Analysis of O’Connor proof.

MY COMMENT

O’Connor states that I have not correctly filled in the details of Gödel’s outline proof of Proposition V. Yet he has not given any detailed reasons to support this contention. He refers to my ‘attempt to find a flaw’ as if to imply that I was attempting to find a flaw but did not actually demonstrate any flaw, when the truth is that I did demonstrate a flaw, and did so in considerable detail.

My paper demonstrates in detail a ‘proof’ (Section 8) that arrives at an expression of Gödel’s Proposition VI (8.5.9 - 8.5.15), based on Gödel’s outline proof. O’Connor claims that I have not done this correctly, but fails to show which steps do not follow Gödel’s outline proof.

I then show (10.1 - 10.3) that the errors in this ‘proof’ occur because Gödel treats number-theoretic relations as expressions both of a sub-language, and of the meta-language. I then demonstrate (10.4) the contradictions that arise from this, contradictions that invalidate the proof.

O’Connor has continued to avoid actually showing where I might have made an erroneous step in my demonstration. Yet again, he simply avoids any detailed reference to my paper at all, and simply introduces irrelevant references to terms from his own paper such as “the ‘evaluation’ function” a term which does not occur either in my paper or Gödel’s paper.

In addition, O’Connor seems to believe that because there are ‘versions’ of Gödel’s proof that have been computer verified that that gives some sort of incontrovertible assurance that there cannot be a flaw in Gödel’s proof. It does nothing of the sort. Simply because a limited number of steps of a ‘proof’ has been ‘checked’ by some computer program can never show that the mathematical system that is being used can never result in any contradiction.

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

I followed Gödel’s usage of the logical implication symbol (⇒). O’Connor does not indicate why or where my usage is incorrect. My paper is readily accessible for any reader who understands English and basic logic. O’Connor has the effrontery to criticize the use of one symbol in my paper, while at the same he refuses to publish a version of his proof in a standard language and format that would be widely known, relying instead on computer code that is not widely known. He expects anyone who wants to know what it is all about to learn this language and continues to hide his ‘proof’ behind this language, a language which is not familiar to the majority.

O’Connor refers to an implicit assumption that the ‘inner axiom system’ is sound, but fails to indicate what he thinks this is or why this might be an error. My demonstration of the flaw in Gödel’s proof is not dependent on the actual formal system used by Gödel in his paper, and would apply for any such formal system (that is, any system that Gödel’s paper claims to apply to, which is essentially all formal systems that include arithmetic), regardless of the ‘soundness’ or otherwise of its axioms.

When he says that I “assume that the logic of the inner system is identical to the logic of the meta-system” he appears to be saying the logic is different for whatever he means by ‘inner system’ and ‘meta-system’, but he doesn’t say what those differences might be, nor give any detail to substantiate his claim of an error in my paper on these grounds.

Finally, he says that he has “uncovered the essential errors in my reasoning”. Isn’t it surprising that he didn’t communicate them in his review? The article Flawed Disproofs shows how easy it is to demonstrate that a disproof of Gödel’s proof is wrong - if it actually is.

## MY CONCLUDING RESPONSE

At no point does O’Connor give any detailed analysis of my paper, at no point does he pinpoint any specific flaw in my main argument. Although ostensibly a ‘review’ of my paper, it would appear to be have been used as an opportunity for O’Connor to eulogise what he calls his formalized proof of Gödel’s theorem.

Note that O’Connor devotes approx 1460 words to his ‘review’. Of those, just 310 words are spent on my main argument – about one fifth of his ‘review’ that dismisses my paper is written about my main argument. And of those 310 words approximately half are simply references to his own paper, and are meaningless unless one were to digest his what he calls his ‘formalization’ of Gödel’s proof.
(Note: anyone who is interested in examining O’Connor’s proof will have to examine 46 files, 7036 lines of specifications, 37906 lines of proof, and 1267747 total characters – and if they do not know the language in which it is all written, they will have to learn that as well. This makes the task of examining O’Connor’s proof far more involved than examining Gödel’s proof, which is in 1 file, with less than 60000 characters, including spaces. **Update: O’Connor’s proof has been examined and a fundamental error has been discovered in it. The details can be seen at Analysis of O’Connor proof.**

My paper is clearly divided into sections and subsections and most of the important lines are numbered in the format (X.X.X) for (Section. Subsection. Line). The only point at which O’Connor claims to pinpoint an error is in his reference to line 9.1.18 of my simplified version of Gödel’s proof, where his claim that there exists an error is laughable (as shown above). And in any case, as already noted, my simplified version of Gödel’s proof is not actually necessary to my demonstration of the flaw in Gödel’s proof, as is noted at the start of Section 10 in my paper.

It speaks for itself when the only point where O’Connor thinks he can locate an error in my paper is an instance where he is clearly mistaken. O’Connor has failed to show where in my demonstration of the flaw in Gödel’s proof my ‘alleged’ errors occur.

### Some further relevant information

O’Connor has criticized me for supposedly not using the ‘correct statement of Gödel’s theorem’, when as noted above, he seems to be unclear as to whether by ‘correct statement of Gödel’s theorem’ he means the generalized theorem or the theorem for one particular formal system.

For this reason I asked him in an e-mail:

“Incidentally, you state that the correct modern version of Gödel’s theorem states that for any sufficiently powerful recursive set of axioms that is (omega-)consistent, there is a (Pi_1) sentence that is unprovable, and whose negation is also unprovable…

Perhaps you would be good enough to tell me how the notions ‘set of axioms’ and ‘sufficiently powerful’ in the above are represented in your formalization. I can’t see it in any of your information that I have seen so far.”

His answer was:

“The sufficiently powerful system I have used is one that I got from Hodel’s book on Logic. He calls the system NN, and the system consists of the following axioms…”

This indicates that despite claiming that he knows the ‘correct statement of Gödel’s theorem’, and is content to criticise others on that basis, he fails to distinguish the essential difference between the generalized theorem and the theorem for one particular formal system.

The same error occurs on his web page (Essential Incompleteness of Arithmetic Verified by Coq) on his ‘formalization’ of “Gödel’s incompleteness theorem”, which claims that his ‘formalization’ is a proof of the generalized theorem, whereas it is plainly evident that whatever it is, it is not a proof of the generalized theorem.

### Computer verified proofs

O’Connor appears to set great importance upon the fact that his ‘proof ’ has been ‘verified’ by a computer program. The uninitiated might accept O’Connor’s apparent claim that a proof that is step by step checked by a computer program must always be infallibly correct. While it is true that such a computer program will always follow the instructions it has been given, to accept the infallibility of program is to rely on the assumption that the creators of the program have not made any mistakes; this includes both the creators of the underlying system and the creators of any specific proof that uses that system.

Furthermore, there is the question of the interpretation of the complete code. The claim of “computer verified proofs” can never assure us that there is no error in the overall reasoning, which is the formalization itself and the interpretation that we put on that formalization. And the more complex the formalization, the more difficult it is to be sure that we have applied the correct interpretation to it.

And, as in O’Connor’s own case, we have to be very careful to check that what the creator of the computer proof claims that the computer proof proves is, in fact what he actually proves. In O’Connor’s case, he claims, among other things, that his computer proof proves that the formal system can express certain expressions - but if one actually looks at the computer code, one will see that it only proves that these certain expressions satisfy a definition made by O’Connor and which he calls “representability”- and then simply assumes that this is the same as the computer actually proving that these certain expressions can be expressed by the computer system. While I would not wish to accuse O’Connor of any deliberate dishonesty, to call such a proof a fully computer checked proof is a gross misrepresentation of the truth. See Representability, and my paper Analysis of O’Connor proof, where this is now addressed.

Also see the article on computer-checked proofs.

Incidentally, there is an interesting snippet on one of O’Connor’s web pages Formal Proofs for Assignments, where he states that a Teaching Assistant was not happy about one of O’Connor’s computer verified proofs, writing:

“You mean we should convert the clear statements […] into an enormous jumble of nonsense and plug that into a device of gargantuan complexity that we have no hope of ever understanding in complete detail?”

The crucial point is that it is pointless to claim that you understand something completely unless you can communicate that understanding to other people. If you want other people to accept that your understanding is valid, you must be able to communicate that understanding to them. If you refuse to communicate in a commonly accepted language, don’t be surprised if other people don’t accept your claims.

Finally, O’Connor has said that I am

*“… so blindingly convinced that Gödel’s theorem is wrong that even when faced with three solid computer verified proofs of the theorem he still refuses to believe he is wrong.”*

Really? These three supposedly solid computer verified proofs have very obvious errors, and I would be blind if I ignored those errors. See:

*PDF An Error in a Computer Verified Proof of Incompleteness by John Harrison**PDF An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor**PDF An Error in a Computer Verified Proof of Incompleteness by Natarajan Shankar*

When the flaws in their proofs were pointed out, the authors were unable to find any error in the description of the flaws - details are given in the above papers.

To claim that I am blind while at the same time refusing to point out any logical error in my argument is rather rich. Perhaps it is O’Connor who should be examining his own deep-seated convictions.

### Another reference to my paper by O’Connor

O’Connor has published another web page on my demonstration of the flaw in Gödel’s proof at “James R Meyer vs Kurt Gödel”.

Here he freely admits to not having a sufficient knowledge of Gödel’s proof to be able to make a viable critique of my paper. It’s rather unfortunate that he didn’t realise that in the first instance.

In this blog page, O’Connor refers to an online discussion, and considers that a certain contributor makes a better argument against me than O’Connor himself could. So, instead of actually revealing my alleged errors, O’Connor directs the reader to a web forum which has 173 posts. This is a well-known deflection ploy where O’Connor hopes that the reader will accept O’Connor’s word for it rather than actually expecting the reader to plough through all these posts in order to find the alleged errors. If the alleged errors are so simple to reveal, then why did O’Connor not simply state them on his blog page? Unlike O’Connor, I am not afraid to give details - I give the details regarding this web forum at On web forums and Gödel’s proof.

I stopped contributing to that forum when it became evident that it was the online equivalent of a bar discussion at closing time, where the other contributors were more interested in point scoring and hurling insults, and where the loudest voices were from those who were unwilling to engage in reasoned discussion. I gave a final posting (Google groups sci.math forum) on that thread which details just one of the errors from the contributor that O’Connor rates so highly. Also see my page On web forums and Gödel’s proof.

In his blog, O’Connor says that he felt relieved when he read this forum discussion. Quite why a discussion that was so full of errors should make him feel relieved is a mystery.

Later in the page, O’Connor goes on to suggest that my demonstration of a flaw in Gödel’s proof is on a par with conspiracy theories such as the notion that there was no moon landing, or to claims of a link between MMR vaccines and autism. Conspiracy theories are theories based on physical events that happened in the past, and the physical evidence of details of the past is always incomplete and often subjective, and that can make it difficult to refute such theories. But my demonstration of a flaw in Gödel’s proof is a purely logical argument and all one has to do to prove me wrong is to find an error in the logic of my argument. That’s what people have done with many such arguments. As an example, see Flawed Disproofs which shows how easy it is to show that a disproof of Gödel’s proof is wrong when you understand the proof - if the disproof actually is flawed.

Rationale: Every logical argument must be defined in some language, and every language has limitations. Attempting to construct a logical argument while ignoring how the limitations of language might affect that argument is a bizarre approach. The correct acknowledgment of the interactions of logic and language explains almost all of the paradoxes, and resolves almost all of the contradictions, conundrums, and contentious issues in modern philosophy and mathematics.Site MissionPlease see the menu for numerous articles of interest. Please leave a comment or send an email if you are interested in the material on this site.

Interested in supporting this site?You can help by sharing the site with others. You can also donate at

_{}where there are full details.