Gödel’s Lost Letter

Gödel’s perspective in this letter is a refutation of the simplistic take on Turing’s proof seen so often in the computer science literature. In particular:

After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem

Here is the letter:

“One can obviously easily construct a Turing machine, which for every formula F in first order predicate logic and every natural number n , allows one to decide if there is a proof of F of length n (length = number of symbols). Let \(\psi(F, n)\) be the number of steps the machine requires for this and let \(φ(n) = max_F (F, n)\) . The question is how fast φ(n) grows for an optimal machine. One can show that φ(n) ≥ kn . If there really were a machine with \(φ(n) \sim k·n\) (or even \(\sim k·n^{2}) \), this would have consequences of the greatest importance [Tragweite]. Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine. After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem. Now it seems to me, however, to be completely within the realm of possibility that φ(n) grows that slowly. Since (1) it seems that \(\phi(n)∼ kn \) is the only estimation which one can obtain by a generalization of the proof of the undecidability of the Entscheidungsproblem; and (2) after all \(φ(n) ∼ k·n\) (or \(∼ k· n^2 \)) only means that the number of steps as opposed to trial and error can be reduced from N to log N (or \((log N )^2 )\). However, such strong reductions appear in other finite problems, for example in the computation of the quadratic residue symbol using repeated application of the law of reciprocity. It would be interesting to know, for instance, the situation concerning the determination of primality of a number and how strongly in general the number of steps in finite combinatorial problems can be reduced with respect to simple exhaustive search.”

( Peter Clote’s translation of Godel’s letter to von Neumann from Sam Buss’s paper).

See also Sipser’s paper which has a different translation of the letter.

Here is Turing’s claim:

I propose, therefore, to show that there can be no general process for determining whether a given formula U of the functional calculus Z is provable, i.e. that there can be no machine which, supplied with any one U of these formulae, will eventually say whether U is provable.

It should perhaps be remarked what I shall prove is quite different from the well-known results of Gödel [15]. Gödel has shown that (in the formalism of Principia Mathematica) there are propositions U such that neither U nor –U is provable. As a consequence of this, it is shown that no proof of consistency of Principia Mathematica (or of Z) can be given within that formalism. On the other hand, I shall show that there is no general method which tells whether a given formula U is provable in Z, or, what comes to the same, whether the system consisting of Z with –U adjoined as an extra axiom is consistent.

If the negation of what Gödel has shown had been proved, i.e. if, for each U, either U or –U is provable, then we should have an immediate solution of the Entscheidungsproblem. For we can invent a machine K which will prove consecutively all provable formulae. Sooner or later K will reach either U or –U. If it reaches U, then we know that U is provable. If it reaches –U, then, since Z is consistent (Hilbert and Ackermann, p.65), we know that U is not provable.

Note: fixed Greek symbols March 16 2015

Added Turing quote 10/1/2015