This page is keyboard accessible:
• 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 skip the menu and move to the main content, press Tab after the page loads to reveal a skip button.
• To get back to the top of the page anytime, press the Home key.
• For more information, click here: Accessibility   Close this tip.

Note: Full functionality of this web page requires JavaScript to be enabled in your browser.

Gödel’s Intuitive Error (2)

This page discusses an blunder in a paper by Kurt Gödel (Footnote: Kurt Gödel: “Zum Entscheidungsproblem des logischen Funktionenkalküls.”, Monatshefte für Mathematik, 40.1 (1933): 433-443. (On the decision problem for the functional calculus of logic)) published in 1933. A synopsis of the error can be found in an article by Warren D. Goldfarb, Introductory note to 1932a, 1933i and 1933l. (Footnote: in Kurt Gödel: Volume I, Collected Works (Feferman, Solomon, et al, Publications 1929-1936.", OUP, 1986).)

Goldfarb’s proof of Gödel’s error can be found at The unsolvability of the Gödel class with identity. (Footnote: Warren D. Goldfarb, The unsolvability of the Gödel class with identity, The Journal of Symbolic Logic, 49, pp 1237-1252 (1984).)


Goldfarb shows that Gödel’s error was caused by a reliance on intuition rather than furnishing a detailed proof. It might be noted that his incompleteness proof also relies on one key proposition that Gödel failed to provide a detailed proof for, instead relying on an uncritical intuition - to this day, mathematicians rely unquestioningly on Gödel’s intuitive claim.



In the 1920s and onwards, many mathematicians became interested in considering formulas in relatively abstract terms, so that rather than considering a formula only in relation to the particular formal system that it belongs to, they considered what properties it might have if the same formula structure was used in several different formal systems.


The formulas that they dealt with were mainly formulas that contained one or more quantified variables, and logical operators such as ∧ (and) and ∨ (or), and perhaps constants and other symbols such as = (the equality symbol).


If one can say that a formula is satisfiable, that means that there are some systems in which the formula is “true” (also referred to as true in some interpretations). And if one can say that a formula is valid, that means that it is “true” in all systems (also referred to as true in all interpretations). (Footnote: For an analysis of what “true” might mean as opposed to what provable might mean, see True but unprovable.)


For example, A formula like:

xy((P(x) ∧ P(y)) → P(y))

is valid. It can be read as meaning:

For every x, the proposition P regarding x and the proposition P regarding y imply the proposition P regarding y. This applies regardless of the actual proposition P, and regardless of the values of x and y. So it is decidable that the formula is valid.


One of the main questions that mathematicians were interested in was whether, given a formula of a certain structure, whether it was decidable if a given formula is satisfiable or valid.


Obviously as the complexity of the formulas increases, the difficulty in answering such questions also increases, and the likelihood that intuition will guess the correct answer decreases.


Some details

The formulas that Gödel was dealing with in his paper were formulas that included universal quantifiers ∀ (‘For all’) and existential quantifiers ∃ (‘There exists’) They can include variables, but no functions or constants, and no equality symbol (also sometimes called the identity symbol - not to be confused with the identity function).


In his paper, Gödel looked at formulas of the type ∀∀∃…∃ which include two initial universal quantifiers, followed by and a number of existential quantifiers, but which included no functions or constants, and no equality symbol. He proved the “finite controllability” of the ∀∀∃…∃ class where there is no equality symbol. (Footnote: Goldfarb: The bulk of 1933i is devoted to a question beyond that of decidability. Call a class of quantificational formulas finitely controllable if and only if every satisfiable formula in it has a finite model. A syntactically specified class is decidable if it is finitely controllable, but the converse does not hold in general. Gödel proves the finite controllability of the ∀∀∃…∃ class.
Subsequent to Gödel’s work, other proofs of the finite controllability of the ∀∀∃…∃ class were devised: that of Schütte 1934a independently, and those of Ackermann 1954, Dreben 1962, and Dreben and Goldfarb 1979 in the light of Gödel’s. These proofs are all, at bottom, similar; they rely on at least some of the combinatorial devices Gödel originated, in particular his Lemma 2. Only recently has a proof that dispenses with these devices been formulated (Gurevich and Shelah 1983). Gödel’s combinatorial lemmas have been generalized: Lemma 1 in Aanderaa and Goldfarb 1974 and Lemma 2 in Erdos 1963 (simplified proofs are in Dreben and Goldfarb 1979, Appendix §2). Such generalizations have been applied in finite controllability proofs for other classes of quantificational formulas (Aanderaa and Goldfarb 1974; Dreben and Goldfarb 1979, Chapters 3 and 4).)


In the last sentence of his paper Gödel asserted, without providing any proof whatsoever, that the same method he used for ∀∀∃…∃ formulas could also be applied to ∀∀∃…∃ formulas that also included the equality symbol.


Perhaps it was because Gödel had such a reputation that his inclusion of an unproven assertion was left unquestioned by the journal Monatshefte für Mathematik (incidentally the same journal that had accepted Gödel’s incompleteness paper without questioning the failure to include a proof of a key proposition of that paper). And presumably it was because of Gödel’s reputation that his assertion regarding ∀∀∃…∃ was accepted as correct for thirty years, and was relied on by other mathematicians in to prove other results. But then Stål Aanderaa was able to define some examples of ∀∀∃…∃ formulas where Gödel’s method of proof for ∀∀∃…∃ formulas could not actually work as Gödel had claimed if the formulas contained the equality symbol. (Footnote: Goldfarb: In the last sentence of 1933i Gödel claims, with no substantiation, that the same method as used for the ∀∀∃…∃ class suffices to show the finite controllability of the ∀∀∃…∃ class extended by the inclusion of the identity sign “=” in the language. In the mid-1960s, however, Stål Aanderaa devised some examples that showed the Gödel-Kalmár-Schütte Criterion not to be sufficient for the satisfiability of ∀∀∃…∃ formulas that contain “=”.)


As Gödel was still alive, he was asked about the final assertion of his paper, and why there appeared to be a difficulty with it, and he eventually changed his claim to a claim that the method of his proof would still apply to a particular subset of ∀∀∃…∃ formulas with the equality symbol. (Footnote: Goldfarb: Gödel, 19 July 1966,
I am sorry I don’t have any notes about the exact procedure for proving Theorem 1 of my paper in case the formula contains “=”. However, I remember that the idea was to formulate the auxiliary concepts and the lemmas under the assumption that in addition to the relations Fi an equivalence relation leaving the Fi invariant is given. No difficulty arose in carrying this through.
Gödel let the matter rest there until 1970. Then, on 3 April 1970, Dana Scott wrote to Dreben and to Hao Wang:
In a recent telephone conversation [Gödel] mentioned that he was able to recall the method by which he dealt with the presence of equality in the matrix of the formula in his solvable prefix class. Since both of you have thought about this question, he asked me to write you the idea.
The idea Scott presents is fairly simple. Let, for example, F = ∀xyz1H; then one can easily find a formula G equivalent to F over universes of cardinality ≥ 4 that has the form
(*)      xy[xy → ∃z1z2 (z1y & z2x & z2y & J )]
where J is a quantifier-free formula that lacks the identity sign. If we use special quantifiers (called “sharp” by Scott) that demand that the value of each quantified variable be distinct from the values of the previous quantified variables, then G can be written
(**)      #x#y#z1#z2J
Scott continues,
Finally, Gödel claims that his original method applies unchanged to sharp formulas.”
Unfortunately, this assertion is false. For, if we apply the Gödel-Kalmár-Schütte Criterion to G by treating J as though it were the matrix of G, then the Criterion fails to be necessary for satisfiability. If, on the other hand, we apply the Criterion to G and take the matrix to be that of a prenex form of (*), which does contain “=”, then the Criterion is not sufficient for satisfiability.)


Unfortunately, it turned out that this both his original assertion and his new modified assertion were both incorrect. Fifty years after Gödel’s paper, Warren D. Goldfarb showed that not only had Gödel made an error in assuming that his proof method would work when the equality symbol was included, but that his intuitive assumption was completely wrong - Goldfarb proved the complete opposite of what Gödel had assumed to be correct (the satisfiability of ∀∀∃…∃ formulas with the equality symbol is not decidable). (Footnote: Goldfarb: By the early 1970s it had become widely recognized that the decision problem for the ∀∀∃…∃ class with identity was open. It was settled in 1983 by the present author.
Contrary to Gödel’s claim, this class is undecidable; indeed, even the ∀∀∃ class with identity is undecidable (Goldfarb 1984, 1984a). The heart of the undecidability proof is the construction of a satisfiable formula F in the ∀∀∃ class with identity with the following property: for some dyadic predicate letter S of F , every model for F contains an ω-sequence a0, a1, a2, … of distinct elements on which the interpretation of S must be that of "successor". This shows at once that the ∀∀∃ class with identity is not finitely controllable. Moreover, the formula F may be exploited to obtain encodings, by ∀∀∃ formulas with identity, of computational processes whose halting problem is undecidable.)



In mathematics, nothing should ever be taken for granted, nothing should ever be assumed to be correct. This applies regardless of the reputation of the mathematician making an assertion. Humans are fallible, and though intuition can often be correct, it can also be wrong. (Footnote: Note that I do not claim to have analyzed the above papers, and hence I cannot be sure that everything referred to is correct. But the principal point - that one should never use an assumption in place of a logical proof - remains valid.)






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



Please wait for comments to load …  


The Lighter Side



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.



New page on Chaitin’s Constant

There is now a new page on Chaitin’s Constant (Chaitin’s Omega), which demonstrates that Chaitin has failed to prove that it is actually algorithmically irreducible.


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:

Gödel 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.




Comments on this site are welcome, please see the comment section.


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.


Copyright © James R Meyer 2012 - 2018