Gödel’s Intuitive Error No.2

This page discusses a blunder in a paper (Footnote: Kurt Gödel: “Zum Entscheidungsproblem des logischen Funktionenkalküls.”, Monatshefte für Mathematik, 40.1 (1933): 433-443, doi:10.1007/BF01708881. (On the decision problem for the functional calculus of logic)) published in 1933 by Kurt Gödel, a proponent of intelligent design (see Statements by Kurt Gödel). A synopsis of the error can be found in the short article Introductory note to 1932a, 1933i and 1933l by Warren D. Goldfarb, (Footnote: Warren D. Goldfarb, Introductory note to 1932a, 1933i and 1933l: published in Kurt Gödel: Volume I, Collected Works (Feferman, Solomon, et al, Publications 1929-1936, OUP, 1986).) and Goldfarb’s proof of the error in Gödel’s paper is available online at PDF The unsolvability of the Gödel class with identity. (Footnote: Warren D. Goldfarb, PDF The unsolvability of the Gödel class with identity, The Journal of Symbolic Logic, 49, pp 1237-1252 (1984), see The unsolvability of the Gödel class with identity: details.)

Kurt Gödel

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 - and, astonishingly, to this day, mathematicians still rely unquestioningly on Gödel’s intuitive claim, see Gödel’s Incompleteness Theorem.

Background

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:

∀x∀y((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 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 order 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 F_i an equivalence relation leaving the F_i 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 = ∀x∀y∃z₁ H; then one can easily find a formula G equivalent to F over universes of cardinality ≥ 4 that has the form:
(*)   ∀x∀y[x ≠ y → ∃z₁∃z₂ (z₁ ≠ y & z₂ ≠ x & z₂ ≠ y & 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∃^#z₁∃^#z₂ J
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.)

Conclusion

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