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

In 1931 Kurt Gödel published a proof (Footnote: The proof is commonly referred to as Gödel’s proof of incompleteness, you can see an English translation of it here. For some background on it, see Gödel’s proof of incompleteness) that has been hailed as a masterpiece of intellectual ability. (Footnote: The mathematician Von Neumann said in 1951 that Gödel’s proof was:
“Kurt Gödel’s achievement in modern logic is singular and monumental - indeed it is more than a monument, it is a landmark which will remain visible far in space and time.” )
However, Gödel’s proof of incompleteness leads directly to a contradiction. This can be easily shown, as follows: (Footnote: For those with some familiarity with Gödel’s paper, see the Appendix below for a more detailed account.)

The proof refers to a specific formal system P, and states that if the system is consistent, (Footnote: A consistent system is a system that cannot result in a contradiction) then there is a proposition in that system that is not provable by that system, and neither is its negation, i.e., that it is incomplete.

However, the proof also supposedly proves that that proposition is correct (commonly referred to as showing that it is “true”).

Having made a proof for one specific formal system, the proof then proceeds to state that the same proof process can be applied to every formal system that includes a sufficient amount of number theory, so that, given any consistent formal system that includes a sufficient amount of number theory, the proof states there always is a proposition in that system that is not provable by that system. And, as above, the proof supposedly also proves, outside of the formal system, that that proposition is correct.

Since the proof that the proposition is correct - but unprovable in the formal system - is made outside of the formal system, that means that, in order to achieve this, the proof must be doing something very special that no formal system can do. You might expect that logicians and mathematicians would have examined the proof to unearth what this magic ingredient is, but you can search high and low, but no-one has ever found the magic ingredient. And you might expect that this should make people wonder if there is any such magic ingredient, and scrutinize the proof very carefully to see if there might actually be an error in the proof. But no, logicians and mathematicians instead prefer to turn a blind eye to this conundrum.

Now, if the proof for a specific formal system is itself logically valid, then it must be possible to formulate that proof within another fully formal system which itself has a fixed definite set of rules of inference and axioms. (Footnote: The formal system that is being examined necessarily has such as clearly defined set of rules and axioms. If this was not the case then that system would not be clearly defined, and we could not rely on any statements produced by it.)

We can call such a formal system S. Given the system S we can produce another formal system S* simply by replacing every symbol used in the system S by a different symbol, where the systems S and S* have no symbols in common.

According to the claim made by Gödel, the formal system S, provided it is consistent, can prove that there is a proposition A in that system S* that is not provable by that system S* - but it is provable by the system S.

And here’s the contradiction. That proposition A is precisely the same proposition in both the system S and the system S* - it is only the symbols used that are different, but the logic leading to a proof of the proposition A must proceed in exactly the same way for both the system S and S*. And if the proof were correct, one could also use the system S* to prove that there is a proposition (which is exactly the same as the proposition A, but with different symbols) which is not provable in the system S, but is provable in the system S*.

This contradiction shows that any such formal system S that “proves” such a result is inconsistent. It follows that Gödel’s proof is not consistent - since the formal system S (and the formal system S*) is simply a system in which Gödel’s proof is fully formalized.

Given this indication that Gödel’s proof is not consistent, then the obvious thing to do next would appear to be to find where and why Gödel’s proof is flawed. The web-pages Gödel’s Incompleteness Theorem and A simplified explanation of Gödel’s proof give an outline of the flaw in the proof and a full demonstration is given in the paper The Fundamental Flaw in Gödel’s Proof of the Incompleteness Theorem (PDF).

It might be noted that Gödel did not actually provide a proof of the crucial step in his incompleteness proof, he simply assumed it to be correct, and amazingly, other mathematicians and logicians all suspend their critical faculties and accept this mathematical no-no. Intuition should never be a substitute for a rigorous proof. And this isn’t the only case of Gödel making intuitive leaps that later turned out to be incorrect, see also Gödel’s Intuitive Error No.2 where it is shown that Gödel’s intuitive conclusion turned out to be precisely the opposite to the correct conclusion.

Note that there have been various attempts to gloss over the contradiction inherent in Gödel’s poof, but these can be shown to be not based on any logical argument, see for example True but unprovable? and Man versus Machine.

Footnotes:

## Appendix: The details of the contradiction

The following is for readers that have some familiarity with Gödel’s paper. We will follow a translation of Gödel’s proof that is based on Meltzer’s translation. We will call the system that Gödel uses to create his proof the "Proof System S", and the formal system that is the subject of the proof P. Gödel’s proposition V asserts that given a primitive recursive number-theoretic relation R, then the Proof System can generate a formal system formula RF that includes in an equivalent form all the relationships between numbers content that the relation R contains, and can also generate a Gödel number r that is the Gödel number of that formal formula RF. This is a constructive generation of the number r, creating a correspondence between: (Footnote: Which begs the question, what is the definition of a number-theoretic relation, and why does a formula of the formal system not satisfy it? )

1. the primitive recursive number-theoretic relation R, and
2. the formal formula RF, and
3. the number r.

In the following, for convenience, we refer to R only as primitive recursive number-theoretic relations that have one free variable, but the same principle applies for R with multiple free variables.

Gödel’s Proposition V claims that if the formula that results from the substitution of the free variable xR of a primitive recursive relation R(xR) by a specific value n, then if the resultant formula is provable in the Proof System S (is “true”), the corresponding formal formula RF(xF) which has its free variable xF substituted by nF is provable by the formal system P, where nF has the same numerical value as n (provided the number theory of the formal system P is logically identical to the number theory of the Proof System S).

Besides that, the proposition claims that there is a number-theoretic relation that states Bew[Sb(r, u/nf )], where u is the number that corresponds to the variable xF of the formal system P, and that that relation is “true”, if RF(xF) is provable by the formal system P.

In his Proposition VI, Gödel defines a relation:

Q(x,y) = ¬{x Bc [Sb(y, 19/Z(y))]}

and asserts that for all x, by applying his Proposition V (which he assumes to be correct instead of proving it correct), either:

¬{x Bc [Sb(y, 19/Z(y))]} ⇒ Bewc[Sb(q, 17/Z(x) 19/Z(y))]

or

x Bc [Sb(y, 19/Z(y))]       ⇒ Bewc[Neg Sb(q, 17/Z(x) 19/Z(y))]

where q is the Gödel number of a formal formula RF with two free variables, and which corresponds to the relation Q as outlined above.

He then substitutes the y by 17 Gen q to give:

For all x, either:

(A)   ¬{x Bc [Sb(17 Gen q, 19/Z(17 Gen q))]} ⇒ Bewc[Sb(q, 17/Z(x) 19/Z(17 Gen q))]

or

(B)   x Bc [Sb(17 Gen q, 19/Z(17 Gen q))]       ⇒ Bewc[Neg Sb(q, 17/Z(x) 19/Z(17 Gen q))]

He gives Sb(q, 19/Z(17 Gen q)) the designation r, giving: (Footnote: Note: the renaming of Sb(q, 19/Z(17 Gen q)) is immaterial to the principle of the proof. )

For all x, either:

(15)     ¬{x Bc (17 Gen r)} ⇒ Bewc[Sb(r, 17/Z(x))]

or

(16)     x Bc (17 Gen r) ⇒ Bewc[Neg Sb(r, 17/Z(x))]

Gödel concludes that (15) must apply for all x, otherwise there is a contradiction.

But in order for Gödel’ Proof System S to assert that there is a contradiction, it must assert, as is asserted in Gödel’s Proposition V (besides the correspondences noted in i, ii, iii above) that there is a correspondence between:

1. a primitive recursive number-theoretic relation R being “true” in the Proof System S itself, and is provable in that system S, and
2. the corresponding formal formula RF being provable in the formal system P, and
3. the corresponding Gödel number r satisfying the number-theoretic relation Bew.

Given the assertion in the Proof System S that:

For all x, ¬{x Bc (17 Gen r)}

from that, by (15) above it can be proved in the Proof System S that:

For all x, Bewc[Sb(r, 17/Z(x))]

and since the correspondences noted (1, 2, 3 above) necessarily exist in the Proof System S, then the Proof System S can also prove that:

For all x, R(x)

where

R(x) = ¬{x Bc (17 Gen r)}

i.e., R(x) is a primitive recursive number-theoretic relation that corresponds to the Gödel number r. (Footnote: Note that there have been numerous cases where it has been claimed that a human can see the truth of the assertion that R(x)) applies for all x, but that no formal system could do so. This is, of course, complete hogwash - if the human is using a completely logical method of inference, then that method can be replicated formally. See also True but unprovable? and Man versus Machine.

So the Proof System S supposedly proves that while it can prove the relationship between numbers that is given by:

For all x, R(x)

it also proves that the formal system P (the formal system it is examining) cannot prove that same relationship between numbers.

So, applying in the same way the Proof System S to the Proof System S* (where the Proof System S* is as described above, and is exactly the same as the Proof System S except that symbols are different) we find that the Proof System S supposedly proves that it can prove the relationship between numbers given by:

For all x, R(x)

but the formal system Proof System S* cannot prove that same relationship between numbers.

And, applying the Proof System S* to the Proof System S, we find that the Proof System S* supposedly proves that it can prove the very same relationship between numbers given by:

For all x, R(x)

but the formal system Proof System S cannot prove that same relationship between numbers.

And that is the contradiction that is inherent in Gödel’s intuitive “proof”.

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.